Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. tuned whitespace
  2. compile
  3. added 'corec' examples and tests
  4. file header
  5. added two 'corec' examples
  6. document addition of 'corec'
  7. moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
  8. put all 'bnf_*.ML' files together, irrespective of bootstrapping/dependency constraints
Changeset 62698:9d706e37ddab by blanchet:
tuned whitespace
The file was modified src/HOL/Corec_Examples/LFilter.thy (diff)
The file was modified src/HOL/Corec_Examples/Stream_Processor.thy (diff)
The file was modified src/HOL/Corec_Examples/Tests/Merge_Poly.thy (diff)
The file was modified src/HOL/Corec_Examples/Tests/Misc_Poly.thy (diff)
The file was modified src/HOL/Tools/BNF/bnf_axiomatization.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp.ML (diff)
Changeset 62697:84a302ab9147 by blanchet:
compile
The file was modified src/HOL/Datatype_Examples/Lift_BNF.thy (diff)
Changeset 62696:7325d8573fb8 by blanchet:
added 'corec' examples and tests
The file was addedsrc/HOL/Corec_Examples/Tests/GPV_Bare_Bones.thy
The file was addedsrc/HOL/Corec_Examples/Tests/Merge_A.thy
The file was addedsrc/HOL/Corec_Examples/Tests/Merge_B.thy
The file was addedsrc/HOL/Corec_Examples/Tests/Merge_C.thy
The file was addedsrc/HOL/Corec_Examples/Tests/Merge_D.thy
The file was addedsrc/HOL/Corec_Examples/Tests/Merge_Poly.thy
The file was addedsrc/HOL/Corec_Examples/Tests/Misc_Mono.thy
The file was addedsrc/HOL/Corec_Examples/Tests/Misc_Poly.thy
The file was addedsrc/HOL/Corec_Examples/Tests/Simple_Nesting.thy
The file was addedsrc/HOL/Corec_Examples/Tests/Small_Concrete.thy
The file was addedsrc/HOL/Corec_Examples/Tests/TLList_Friends.thy
The file was modified src/HOL/ROOT (diff)
Changeset 62695:b287b56a6ce5 by blanchet:
file header
The file was modified src/HOL/Datatype_Examples/Lift_BNF.thy (diff)
Changeset 62694:f50d7efc8fe3 by blanchet:
added two 'corec' examples
The file was addedsrc/HOL/Corec_Examples/LFilter.thy
The file was addedsrc/HOL/Corec_Examples/Stream_Processor.thy
The file was modified src/HOL/Datatype_Examples/Stream_Processor.thy (diff)
The file was modified src/HOL/ROOT (diff)
Changeset 62693:0ae225877b68 by blanchet:
document addition of 'corec'
The file was modified CONTRIBUTORS (diff)
The file was modified NEWS (diff)
Changeset 62692:0701f25fac39 by blanchet:
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
The file was addedsrc/HOL/Library/BNF_Corec.thy
The file was addedsrc/HOL/Tools/BNF/bnf_gfp_grec.ML
The file was addedsrc/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
The file was addedsrc/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML
The file was addedsrc/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML
The file was addedsrc/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML
The file was addedsrc/HOL/Tools/BNF/bnf_gfp_grec_unique_sugar.ML
The file was modified src/HOL/Library/Library.thy (diff)
Changeset 62691:9bfcbab7cd99 by blanchet:
put all 'bnf_*.ML' files together, irrespective of bootstrapping/dependency constraints
The file was addedsrc/HOL/Tools/BNF/bnf_axiomatization.ML
The file was addedsrc/HOL/Tools/BNF/bnf_lfp_countable.ML
The file was modified src/HOL/Library/BNF_Axiomatization.thy (diff)
The file was modified src/HOL/Library/Countable.thy (diff)
The file was removedsrc/HOL/Library/bnf_axiomatization.ML
The file was removedsrc/HOL/Library/bnf_lfp_countable.ML