Summary
- clarified heading
- a quasi-recursive characterization of the multiset order (by Christian Sternagel)
- merged
- avoid spurious fact index, notably in "context begin" (via Bundle.context);
- tuned;
- tuned;
- tuned;
The file was modified | src/HOL/Library/Multiset.thy (diff) |
The file was modified | src/HOL/Library/Multiset.thy (diff) |
The file was modified | src/HOL/Wellfounded.thy (diff) |
The file was modified | src/Pure/Isar/expression.ML (diff) |
The file was modified | src/Pure/Isar/expression.ML (diff) |
The file was modified | src/Pure/Isar/expression.ML (diff) |
The file was modified | src/Pure/Isar/proof_context.ML (diff) |