Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. lift BNF witnesses for quotients (unless better ones are specified by the user)
  3. more robust (amending add9a9f6a290): proper syntax error instead of exception for grammar with unreachable nonterminals, e.g. nonterminal f1 syntax "_F" :: "f1 ⇒ 'b" ("F _" 10);
  4. merged
  5. tuned var names (avoid h)
  6. more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
  7. a few new lemmas
Changeset 71470:b94053ca8d77 by traytel:
merged
Changeset 71469:d7ef73df3d15 by traytel:
lift BNF witnesses for quotients (unless better ones are specified by the user)
The file was modified src/HOL/Datatype_Examples/Cyclic_List.thy (diff)
The file was modified src/HOL/Datatype_Examples/Dlist.thy (diff)
The file was modified src/HOL/Datatype_Examples/Free_Idempotent_Monoid.thy (diff)
The file was modified src/HOL/Datatype_Examples/LDL.thy (diff)
The file was modified src/HOL/Datatype_Examples/Lift_BNF.thy (diff)
The file was modified src/HOL/Datatype_Examples/TLList.thy (diff)
The file was modified src/HOL/Tools/BNF/bnf_lift.ML (diff)
Changeset 71468:53fcbede7bf7 by wenzelm:
more robust (amending add9a9f6a290): proper syntax error instead of exception for grammar with unreachable nonterminals, e.g. nonterminal f1 syntax "_F" :: "f1 ⇒ 'b"  ("F _" 10);
The file was modified src/Pure/Syntax/parser.ML (diff)
Changeset 71467:708d301205fe by nipkow:
merged
Changeset 71466:ac70b63785bb by nipkow:
tuned var names (avoid h)
The file was modified src/HOL/Data_Structures/AVL_Set.thy (diff)
Changeset 71465:910a081cca74 by wenzelm:
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
The file was modified src/Doc/Implementation/Logic.thy (diff)
The file was modified src/HOL/ex/Iff_Oracle.thy (diff)
The file was modified src/Pure/General/position.ML (diff)
The file was modified src/Pure/General/pretty.ML (diff)
The file was modified src/Pure/General/properties.ML (diff)
The file was modified src/Pure/Proof/extraction.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
The file was modified src/Pure/thm.ML (diff)
The file was modified src/Pure/thm_deps.ML (diff)
Changeset 71464:4a04b6bd628b by paulson _lp15@cam.ac.uk_:
a few new lemmas
The file was modified src/HOL/Fun.thy (diff)
The file was modified src/HOL/Library/Ramsey.thy (diff)