Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. merged
  2. tuned;
  3. allow 'for' fixes for multi_specs;
  4. unused;
  5. clarified check_open_spec / read_open_spec; allow 'for' fixes in 'abbreviation', 'definition';
  6. tuned;
  7. clarified 'axiomatization';
  8. clarified axiomatization;
  9. clarified axiomatization: proper variables (!);
Changeset 63184:dd6cd88cebd9 by wenzelm:
merged
Changeset 63183:4d04e14d7ab8 by wenzelm:
tuned;
The file was modified src/Doc/Isar_Ref/HOL_Specific.thy (diff)
The file was modified src/Doc/Isar_Ref/Outer_Syntax.thy (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML (diff)
The file was modified src/HOL/Tools/Function/fun.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/Pure/Isar/parse_spec.ML (diff)
Changeset 63182:b065b4833092 by wenzelm:
allow 'for' fixes for multi_specs;
The file was modified src/Doc/Isar_Ref/HOL_Specific.thy (diff)
The file was modified src/Doc/Isar_Ref/Outer_Syntax.thy (diff)
The file was modified src/Doc/Isar_Ref/Spec.thy (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/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/Function/partial_function.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/quickcheck_common.ML (diff)
The file was modified src/Pure/Isar/parse_spec.ML (diff)
The file was modified src/Pure/Isar/specification.ML (diff)
Changeset 63181:ee1c9de4e03a by wenzelm:
unused;
The file was modified src/Pure/Isar/specification.ML (diff)
Changeset 63180:ddfd021884b4 by wenzelm:
clarified check_open_spec / read_open_spec;<br>allow &#039;for&#039; fixes in &#039;abbreviation&#039;, &#039;definition&#039;;
The file was modified NEWS (diff)
The file was modified src/Doc/Isar_Ref/Spec.thy (diff)
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/SPARK/Tools/spark_vcs.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/Lifting/lifting_setup.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/narrowing_generators.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/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)
Changeset 63179:231e261fd6bc by wenzelm:
tuned;
The file was modified src/Pure/Isar/specification.ML (diff)
Changeset 63178:b9e1d53124f5 by wenzelm:
clarified &#039;axiomatization&#039;;
The file was modified NEWS (diff)
The file was modified src/Doc/Isar_Ref/Spec.thy (diff)
The file was modified src/Doc/Tutorial/Misc/AdvancedInd.thy (diff)
The file was modified src/HOL/Tools/BNF/bnf_axiomatization.ML (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/Tools/Code/code_runtime.ML (diff)
Changeset 63177:6c05c4632949 by wenzelm:
clarified axiomatization;
The file was modified src/HOL/Quickcheck_Examples/Hotel_Example.thy (diff)
Changeset 63176:878bd5922f3b by wenzelm:
clarified axiomatization: proper variables (!);
The file was modified src/HOL/MicroJava/J/JListExample.thy (diff)