Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned;
  2. clarified signature;
  3. misc tuning and clarification; removed unused all_registrations_of;
  4. clarified signature;
  5. more explicit instantiate_morphism (without checks for typ / term component);
  6. tuned;
  7. tuned signature;
Changeset 67655:8f4810b9d9d1 by wenzelm:
tuned;
The file was modified src/Pure/Isar/locale.ML (diff)
Changeset 67654:49f45fcd335b by wenzelm:
clarified signature;
The file was modified src/Pure/Isar/generic_target.ML (diff)
The file was modified src/Pure/Isar/locale.ML (diff)
Changeset 67653:4ba01fea9cfd by wenzelm:
misc tuning and clarification;<br>removed unused all_registrations_of;
The file was modified src/Pure/Isar/locale.ML (diff)
Changeset 67652:11716a084cae by wenzelm:
clarified signature;
The file was modified src/Pure/Isar/attrib.ML (diff)
The file was modified src/Pure/Isar/bundle.ML (diff)
The file was modified src/Pure/Isar/generic_target.ML (diff)
The file was modified src/Pure/Isar/local_theory.ML (diff)
The file was modified src/Pure/Isar/locale.ML (diff)
The file was modified src/Pure/Isar/token.ML (diff)
Changeset 67651:6dd41193a72a by wenzelm:
more explicit instantiate_morphism (without checks for typ / term component);
The file was modified src/HOL/Tools/Function/function_common.ML (diff)
The file was modified src/Pure/morphism.ML (diff)
Changeset 67650:5e4f9a0ffea5 by wenzelm:
tuned;
The file was modified src/Pure/morphism.ML (diff)
Changeset 67649:1e1782c1aedf by wenzelm:
tuned signature;
The file was modified src/HOL/Decision_Procs/Commutative_Ring.thy (diff)
The file was modified src/HOL/Decision_Procs/Reflective_Field.thy (diff)
The file was modified src/HOL/Library/conditional_parametricity.ML (diff)
The file was modified src/HOL/Probability/Giry_Monad.thy (diff)
The file was modified src/HOL/Tools/Function/function_context_tree.ML (diff)
The file was modified src/HOL/Tools/inductive.ML (diff)
The file was modified src/HOL/Tools/lin_arith.ML (diff)
The file was modified src/Provers/Arith/fast_lin_arith.ML (diff)
The file was modified src/Provers/classical.ML (diff)
The file was modified src/Provers/splitter.ML (diff)
The file was modified src/Pure/Isar/code.ML (diff)
The file was modified src/Pure/Isar/context_rules.ML (diff)
The file was modified src/Pure/Isar/locale.ML (diff)
The file was modified src/Pure/Isar/spec_rules.ML (diff)
The file was modified src/Pure/Isar/subgoal.ML (diff)
The file was modified src/Pure/Proof/proof_syntax.ML (diff)
The file was modified src/Pure/Proof/reconstruct.ML (diff)
The file was modified src/Pure/Tools/named_theorems.ML (diff)
The file was modified src/Pure/facts.ML (diff)
The file was modified src/Pure/more_thm.ML (diff)
The file was modified src/Pure/raw_simplifier.ML (diff)
The file was modified src/Pure/thm.ML (diff)
The file was modified src/Tools/Code/code_runtime.ML (diff)
The file was modified src/Tools/induct.ML (diff)