Changes

Summary

tuned;
minor performance tuning;
NEWS and example for Theory.join_theory;
tuned whitespace;
more compact proof terms;
more documentation;
added SUBPROOFS / "subproofs" method combinator, for more compact proofterms;
clarified modules;

Changeset 70527:095e6459d3da by wenzelm: tuned;
The file was modified	`src/Provers/Arith/cancel_numeral_factor.ML` (diff)
The file was modified	`src/Provers/Arith/cancel_numerals.ML` (diff)
The file was modified	`src/Provers/Arith/combine_numerals.ML` (diff)
Changeset 70526:bb18c7ac9cff by wenzelm: minor performance tuning;
The file was modified	`src/Pure/Syntax/syntax.ML` (diff)
Changeset 70525:1615b6808192 by wenzelm: NEWS and example for Theory.join_theory;
The file was added	`src/HOL/ex/Join_Theory.thy`
The file was modified	`NEWS` (diff)
The file was modified	`src/HOL/ROOT` (diff)
Changeset 70524:7783bece74b4 by wenzelm: tuned whitespace;
The file was modified	`NEWS` (diff)
Changeset 70523:1182ea5c9a6e by wenzelm: more compact proof terms;
The file was modified	`src/HOL/Enum.thy` (diff)
Changeset 70522:f2d58cafbc13 by wenzelm: more documentation;
The file was modified	`NEWS` (diff)
The file was modified	`src/Doc/Isar_Ref/Proof.thy` (diff)
Changeset 70521:9ddd66d53130 by wenzelm: added SUBPROOFS / "subproofs" method combinator, for more compact proofterms;
The file was modified	`src/Pure/Isar/method.ML` (diff)
The file was modified	`src/Pure/ROOT.ML` (diff)
The file was modified	`src/Pure/context_tactic.ML` (diff)
The file was modified	`src/Pure/par_tactical.ML` (diff)
Changeset 70520:11d8517d9384 by wenzelm: clarified modules;
The file was added	`src/Pure/context_tactic.ML`
The file was modified	`src/HOL/Eisbach/Eisbach.thy` (diff)
The file was modified	`src/HOL/Fun_Def.thy` (diff)
The file was modified	`src/HOL/Nominal/nominal_primrec.ML` (diff)
The file was modified	`src/HOL/Tools/coinduction.ML` (diff)
The file was modified	`src/Pure/Isar/element.ML` (diff)
The file was modified	`src/Pure/Isar/method.ML` (diff)
The file was modified	`src/Pure/Isar/proof.ML` (diff)
The file was modified	`src/Pure/ROOT.ML` (diff)
The file was modified	`src/Tools/induct.ML` (diff)
The file was modified	`src/Tools/induction.ML` (diff)