Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned;
  2. NEWS;
  3. clarified order: params/prems/concl interchangeable with !!/==> proposition;
  4. support 'assumes' in specifications, e.g. 'definition', 'inductive'; tuned signatures;
  5. tuned;
Changeset 63067:0a8a75e400da by wenzelm:
tuned;
The file was modified src/HOL/Induct/Sigma_Algebra.thy (diff)
The file was modified src/HOL/Isar_Examples/Mutilated_Checkerboard.thy (diff)
The file was modified src/HOL/Unix/Unix.thy (diff)
The file was modified src/HOL/ex/Functions.thy (diff)
Changeset 63066:4b0ad6c5d1ca by wenzelm:
NEWS;
The file was modified NEWS (diff)
Changeset 63065:3cb7b06d0a9f by wenzelm:
clarified order: params/prems/concl interchangeable with !!/==> proposition;
The file was modified src/Pure/Isar/specification.ML (diff)
Changeset 63064:2f18172214c8 by wenzelm:
support &#039;assumes&#039; in specifications, e.g. &#039;definition&#039;, &#039;inductive&#039;;<br>tuned signatures;
The file was modified src/HOL/HOLCF/Tools/cpodef.ML (diff)
The file was modified src/HOL/HOLCF/Tools/domaindef.ML (diff)
The file was modified src/HOL/HOLCF/Tools/fixrec.ML (diff)
The file was modified src/HOL/Nominal/nominal_atoms.ML (diff)
The file was modified src/HOL/Nominal/nominal_datatype.ML (diff)
The file was modified src/HOL/Nominal/nominal_primrec.ML (diff)
The file was modified src/HOL/SPARK/Tools/spark_vcs.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_axiomatization.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_grec.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_grec_sugar.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_compat.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML (diff)
The file was modified src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML (diff)
The file was modified src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML (diff)
The file was modified src/HOL/Tools/Function/fun.ML (diff)
The file was modified src/HOL/Tools/Function/fun_cases.ML (diff)
The file was modified src/HOL/Tools/Function/function.ML (diff)
The file was modified src/HOL/Tools/Function/function_common.ML (diff)
The file was modified src/HOL/Tools/Function/partial_function.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_setup.ML (diff)
The file was modified src/HOL/Tools/Old_Datatype/old_primrec.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/narrowing_generators.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/quickcheck_common.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/random_generators.ML (diff)
The file was modified src/HOL/Tools/code_evaluation.ML (diff)
The file was modified src/HOL/Tools/inductive.ML (diff)
The file was modified src/HOL/Tools/inductive_set.ML (diff)
The file was modified src/HOL/Tools/record.ML (diff)
The file was modified src/HOL/Typerep.thy (diff)
The file was modified src/Pure/Isar/parse_spec.ML (diff)
The file was modified src/Pure/Isar/specification.ML (diff)
The file was modified src/Pure/Pure.thy (diff)
The file was modified src/Pure/ROOT.ML (diff)
The file was modified src/Tools/Code/code_runtime.ML (diff)
Changeset 63063:c9605a284fba by wenzelm:
tuned;
The file was modified src/Pure/Isar/specification.ML (diff)
The file was modified src/Pure/logic.ML (diff)