Changes

Summary

merged
embedded content may be delimited via cartouches;
tuned;

Changeset 63121:284e1802bc5c by wenzelm: merged
Changeset 63120:629a4c5e953e by wenzelm: embedded content may be delimited via cartouches;
The file was modified	`NEWS` (diff)
The file was modified	`src/CCL/CCL.thy` (diff)
The file was modified	`src/CCL/Wfd.thy` (diff)
The file was modified	`src/CTT/CTT.thy` (diff)
The file was modified	`src/Doc/Isar_Ref/Document_Preparation.thy` (diff)
The file was modified	`src/Doc/Isar_Ref/Outer_Syntax.thy` (diff)
The file was modified	`src/Doc/Prog_Prove/LaTeXsugar.thy` (diff)
The file was modified	`src/FOL/FOL.thy` (diff)
The file was modified	`src/HOL/Eisbach/parse_tools.ML` (diff)
The file was modified	`src/HOL/HOLCF/IOA/CompoScheds.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/Sequence.thy` (diff)
The file was modified	`src/HOL/Library/LaTeXsugar.thy` (diff)
The file was modified	`src/HOL/Tools/functor.ML` (diff)
The file was modified	`src/HOL/UNITY/UNITY_Main.thy` (diff)
The file was modified	`src/HOL/ex/Cartouche_Examples.thy` (diff)
The file was modified	`src/LCF/LCF.thy` (diff)
The file was modified	`src/Pure/Isar/args.ML` (diff)
The file was modified	`src/Pure/Isar/parse.ML` (diff)
The file was modified	`src/Pure/ML/ml_antiquotations.ML` (diff)
The file was modified	`src/Pure/ML/ml_thms.ML` (diff)
The file was modified	`src/Pure/Thy/document_antiquotations.ML` (diff)
The file was modified	`src/Pure/Thy/thy_output.ML` (diff)
The file was modified	`src/Pure/Tools/rule_insts.ML` (diff)
The file was modified	`src/Tools/induct_tacs.ML` (diff)
The file was modified	`src/ZF/Tools/ind_cases.ML` (diff)
The file was modified	`src/ZF/Tools/induct_tacs.ML` (diff)
The file was modified	`src/ZF/UNITY/SubstAx.thy` (diff)
Changeset 63119:547460dc5c1e by wenzelm: tuned;
The file was modified	`src/HOL/Tools/Lifting/lifting_setup.ML` (diff)