Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. no printing of axioms -- too bulky;
  2. clarified axiom_table: uniform space (e.g. like consts), e.g. relevant for export of HOL-ex.Join_Theory;
  3. more conservative type names, e.g. relevant for Isabelle/MMT export;
  4. clarified types (again): 'a is canonical for 'class' (as alternative to 'locale'), 'b is common for Hindley-Milner examples;
Changeset 70924:15758fced053 by wenzelm:
no printing of axioms -- too bulky;
The file was modified src/Pure/Isar/proof_display.ML (diff)
Changeset 70923:98d9b78b7f47 by wenzelm:
clarified axiom_table: uniform space (e.g. like consts), e.g. relevant for export of HOL-ex.Join_Theory;
The file was modified src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy (diff)
The file was modified src/HOL/Tools/Nitpick/nitpick_hol.ML (diff)
The file was modified src/Pure/Thy/export_theory.ML (diff)
The file was modified src/Pure/theory.ML (diff)
The file was modified src/Pure/thm.ML (diff)
Changeset 70922:539dfd4c166b by wenzelm:
more conservative type names, e.g. relevant for Isabelle/MMT export;
The file was modified src/Pure/more_thm.ML (diff)
Changeset 70921:05810acd4858 by wenzelm:
clarified types (again): 'a is canonical for 'class' (as alternative to 'locale'), 'b is common for Hindley-Milner examples;
The file was modified src/HOL/ex/Peano_Axioms.thy (diff)