2014-03-18 haftmann [Tue, 18 Mar 2014 22:11:46 +0100] rev 56212
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
NEWS src/HOL/Complete_Lattices.thy src/HOL/Library/Extended_Real.thy src/HOL/Library/Liminf_Limsup.thy src/HOL/Library/Product_Order.thy src/HOL/Library/RBT_Set.thy src/HOL/Lifting_Set.thy src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy src/HOL/Predicate.thy src/HOL/Probability/Borel_Space.thy src/HOL/Probability/Caratheodory.thy src/HOL/Probability/Lebesgue_Integration.thy src/HOL/Probability/Measure_Space.thy src/HOL/Probability/Radon_Nikodym.thy src/HOL/Probability/Regularity.thy

2014-03-18 wenzelm [Tue, 18 Mar 2014 21:02:33 +0100] rev 56211
merged;
src/Pure/System/session.ML src/Pure/System/session.scala src/Pure/Thy/thy_load.ML src/Pure/Thy/thy_load.scala src/Tools/jEdit/src/jedit_thy_load.scala

2014-03-18 wenzelm [Tue, 18 Mar 2014 18:09:31 +0100] rev 56210
clarified module arrangement;
src/Pure/PIDE/session.ML src/Pure/PIDE/session.scala src/Pure/ROOT src/Pure/ROOT.ML src/Pure/System/session.ML src/Pure/System/session.scala src/Pure/build-jars

2014-03-18 wenzelm [Tue, 18 Mar 2014 17:53:40 +0100] rev 56209
simplified (despite 70898d016538);
src/Pure/Isar/parse.scala src/Pure/PIDE/resources.scala

2014-03-18 wenzelm [Tue, 18 Mar 2014 17:39:03 +0100] rev 56208
clarifed module name;
src/Doc/Codegen/Setup.thy src/Doc/Tutorial/ToyList/ToyList_Test.thy src/Doc/antiquote_setup.ML src/HOL/SMT_Examples/boogie.ML src/HOL/SPARK/Tools/spark_commands.ML src/HOL/Tools/SMT/smt_config.ML src/HOL/Tools/SMT2/smt2_config.ML src/Pure/Isar/parse.scala src/Pure/PIDE/document.ML src/Pure/PIDE/resources.ML src/Pure/PIDE/resources.scala src/Pure/ROOT src/Pure/ROOT.ML src/Pure/System/session.scala src/Pure/Thy/thy_info.ML src/Pure/Thy/thy_info.scala src/Pure/Thy/thy_load.ML src/Pure/Thy/thy_load.scala src/Pure/Thy/thy_syntax.scala src/Pure/Tools/build.scala src/Pure/Tools/proof_general.ML src/Pure/build-jars src/Pure/pure_syn.ML src/Tools/Code/code_runtime.ML src/Tools/Code/code_target.ML src/Tools/jEdit/lib/Tools/jedit src/Tools/jEdit/src/document_model.scala src/Tools/jEdit/src/find_dockable.scala src/Tools/jEdit/src/isabelle_sidekick.scala src/Tools/jEdit/src/jedit_resources.scala src/Tools/jEdit/src/jedit_thy_load.scala src/Tools/jEdit/src/plugin.scala src/Tools/jEdit/src/rendering.scala src/Tools/jEdit/src/theories_dockable.scala src/Tools/jEdit/src/timing_dockable.scala

2014-03-18 wenzelm [Tue, 18 Mar 2014 16:45:14 +0100] rev 56207
tuned proofs;
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy

2014-03-18 wenzelm [Tue, 18 Mar 2014 16:44:51 +0100] rev 56206
clarified module arrangement;
more antiquotations;
src/Pure/Proof/extraction.ML src/Pure/Proof/proof_syntax.ML src/Pure/ROOT.ML

2014-03-18 wenzelm [Tue, 18 Mar 2014 16:16:28 +0100] rev 56205
clarified modules;
more antiquotations for antiquotations;
NEWS src/Pure/ML/ml_antiquotation.ML src/Pure/ML/ml_antiquotations.ML src/Pure/ML/ml_context.ML src/Pure/ML/ml_thms.ML src/Pure/Pure.thy src/Pure/ROOT.ML src/Tools/Code/code_runtime.ML

2014-03-18 wenzelm [Tue, 18 Mar 2014 15:29:58 +0100] rev 56204
more antiquotations;
src/Pure/Isar/class.ML src/Pure/Isar/code.ML src/Pure/Isar/context_rules.ML src/Pure/Isar/isar_cmd.ML src/Pure/Isar/locale.ML src/Pure/Isar/method.ML src/Pure/Thy/term_style.ML src/Pure/Thy/thy_load.ML src/Pure/Thy/thy_output.ML src/Pure/pure_syn.ML src/Pure/simplifier.ML

2014-03-18 wenzelm [Tue, 18 Mar 2014 13:36:28 +0100] rev 56203
clarified bootstrap process: switch to ML with context and antiquotations earlier;
src/Pure/Isar/outer_syntax.ML src/Pure/ML/ml_context.ML src/Pure/ML/ml_env.ML src/Pure/ROOT.ML src/Pure/Thy/term_style.ML