Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. backed out changeset 1b8858f4c393: odd problems e.g. in CAVA_LTL_Modelchecker;
  3. more careful treatment of implicit context;
  4. clarified signature; more careful treatment of implicit context;
  5. more robust and convenient treatment of implicit context;
  6. clarified context: proper transfer;
  7. tuned;
  8. clarified modules: more direct data implementation;
  9. Added Takeuchi function to HOL-ex
Changeset 70476:5c1b2f616d15 by wenzelm:
merged
Changeset 70475:98b6da301e13 by wenzelm:
backed out changeset 1b8858f4c393: odd problems e.g. in CAVA_LTL_Modelchecker;
The file was modified src/Pure/axclass.ML (diff)
The file was modified src/Pure/thm.ML (diff)
The file was modified src/Tools/Code/code_symbol.ML (diff)
Changeset 70474:235396695401 by wenzelm:
more careful treatment of implicit context;
The file was modified src/ZF/Datatype.thy (diff)
The file was modified src/ZF/Tools/datatype_package.ML (diff)
The file was modified src/ZF/Tools/induct_tacs.ML (diff)
The file was modified src/ZF/Tools/primrec_package.ML (diff)
Changeset 70473:9179e7a98196 by wenzelm:
clarified signature;<br>more careful treatment of implicit context;
The file was modified src/HOL/Tools/Lifting/lifting_def.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_info.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_setup.ML (diff)
The file was modified src/HOL/Tools/Transfer/transfer.ML (diff)
Changeset 70472:cf66d2db97fe by wenzelm:
more robust and convenient treatment of implicit context;
The file was modified src/Pure/drule.ML (diff)
The file was modified src/Pure/raw_simplifier.ML (diff)
The file was modified src/Pure/thm.ML (diff)
Changeset 70471:1004333b76aa by wenzelm:
clarified context: proper transfer;
The file was modified src/Pure/Isar/object_logic.ML (diff)
Changeset 70470:54cebc5cd108 by wenzelm:
tuned;
The file was modified src/ZF/arith_data.ML (diff)
Changeset 70469:1b8858f4c393 by wenzelm:
clarified modules: more direct data implementation;
The file was modified src/Pure/axclass.ML (diff)
The file was modified src/Pure/thm.ML (diff)
The file was modified src/Tools/Code/code_symbol.ML (diff)
Changeset 70468:8406a2c296e0 by manuel eberl _eberlm@in.tum.de_:
Added Takeuchi function to HOL-ex
The file was modified src/HOL/ex/Functions.thy (diff)