Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. proper noWordSep as in "isabelle" mode (cf. 5024d0c48e02);
  2. merged
  3. NEWS;
  4. tuned proofs;
  5. provide dynamic facts in static context, to allow use of method_facts during static closure;
  6. tuned;
  7. clarified signature;
  8. less ambitious arguments: thms only, no context declaration;
  9. added method operator "use";
  10. clarified signature;
  11. clean facts more uniformly;
  12. expode method_facts via dynamic method context;
  13. tuned;
Changeset 63261:90a44d271683 by wenzelm:
proper noWordSep as in "isabelle" mode (cf. 5024d0c48e02);
The file was modified src/Tools/jEdit/src/pretty_text_area.scala (diff)
Changeset 63260:0edec65d0633 by wenzelm:
merged
Changeset 63259:29fe61d5f748 by wenzelm:
NEWS;
The file was modified NEWS (diff)
Changeset 63258:576fb8068ba6 by wenzelm:
tuned proofs;
The file was modified src/HOL/MicroJava/BV/BVNoTypeError.thy (diff)
The file was modified src/HOL/MicroJava/BV/BVSpecTypeSafe.thy (diff)
The file was modified src/HOL/MicroJava/BV/EffectMono.thy (diff)
The file was modified src/HOL/MicroJava/Comp/TypeInf.thy (diff)
The file was modified src/HOL/MicroJava/DFA/Err.thy (diff)
The file was modified src/HOL/MicroJava/DFA/LBVComplete.thy (diff)
The file was modified src/HOL/MicroJava/DFA/LBVSpec.thy (diff)
The file was modified src/HOL/MicroJava/DFA/Semilat.thy (diff)
The file was modified src/HOL/MicroJava/J/JBasis.thy (diff)
Changeset 63257:94d1f820130f by wenzelm:
provide dynamic facts in static context, to allow use of method_facts during static closure;
The file was modified src/Pure/Isar/method.ML (diff)
Changeset 63256:74a4299632ae by wenzelm:
tuned;
The file was modified src/Pure/Isar/method.ML (diff)
Changeset 63255:3f594efa9504 by wenzelm:
clarified signature;
The file was modified src/HOL/Eisbach/method_closure.ML (diff)
The file was modified src/Pure/Isar/proof_context.ML (diff)
The file was modified src/Pure/facts.ML (diff)
Changeset 63254:7bd64a07fe43 by wenzelm:
less ambitious arguments: thms only, no context declaration;
The file was modified src/HOL/Eisbach/Eisbach.thy (diff)
Changeset 63253:d097baa19bd9 by wenzelm:
added method operator "use";
The file was modified src/HOL/Eisbach/Eisbach.thy (diff)
Changeset 63252:1ee45339e86d by wenzelm:
clarified signature;
The file was modified src/Pure/Isar/method.ML (diff)
Changeset 63251:9a20078425b1 by wenzelm:
clean facts more uniformly;
The file was modified src/Pure/Isar/method.ML (diff)
The file was modified src/Pure/Isar/proof.ML (diff)
Changeset 63250:96cfb07c60d4 by wenzelm:
expode method_facts via dynamic method context;
The file was modified src/Pure/Isar/method.ML (diff)
Changeset 63249:d1693d7b0c01 by wenzelm:
tuned;
The file was modified src/Pure/Isar/proof.ML (diff)