2011-05-01 wenzelm 2011-05-01 eliminated copies of isabelle style files;
2011-05-01 wenzelm 2011-05-01 use @{rail} antiquotation (with some nested markup); eliminated separate rail/latex phase;
2011-04-30 wenzelm 2011-04-30 updated Variable.focus;
2011-04-30 wenzelm 2011-04-30 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
2011-04-30 wenzelm 2011-04-30 tuned;
2011-04-30 wenzelm 2011-04-30 more robust error handling (NB: Source.source requires total scanner or recover); tuned;
2011-04-30 wenzelm 2011-04-30 removed old rail.ML;
2011-04-30 wenzelm 2011-04-30 railroad diagrams in LaTeX as document antiquotation;
2011-04-30 wenzelm 2011-04-30 more uniform variations of scan_string;
2011-04-28 wenzelm 2011-04-28 literal facts `prop` may contain dummy patterns;
2011-04-28 wenzelm 2011-04-28 eliminated slightly odd Proof_Context.bind_fixes; tuned;
2011-04-28 berghofe 2011-04-28 merged
2011-04-27 berghofe 2011-04-27 Properly treat proof functions with no arguments.
2011-04-27 wenzelm 2011-04-27 merged
2011-04-27 krauss 2011-04-27 inlined Function_Lib.replace_frees, which is used only once
2011-04-27 wenzelm 2011-04-27 more precise positions via binding;
2011-04-27 wenzelm 2011-04-27 clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
2011-04-27 wenzelm 2011-04-27 tuned signature -- eliminated odd comment;
2011-04-27 wenzelm 2011-04-27 more informative markup for fixed variables (via name space entry); uniform markup for undeclared entities; tuned;
2011-04-27 wenzelm 2011-04-27 discontinued obsolete markup;
2011-04-27 wenzelm 2011-04-27 more precise position information via Variable.add_fixes_binding;
2011-04-27 wenzelm 2011-04-27 more formal treatment of parameters, avoiding slightly odd Variable.intern_fixed;
2011-04-27 wenzelm 2011-04-27 some adhoc renaming, to accomodate more strict checks of fixes (cf. 4638622bcaa1);
2011-04-27 wenzelm 2011-04-27 reorganized fixes as specialized (global) name space;
2011-04-27 wenzelm 2011-04-27 export Name_Space.entry_ord;
2011-04-27 wenzelm 2011-04-27 direct use of Variable.is_fixed;
2011-04-27 wenzelm 2011-04-27 tuned;
2011-04-27 wenzelm 2011-04-27 predefined LaTeX macros for \<bind> and \<then>;
2011-04-27 wenzelm 2011-04-27 eliminated obsolete Function_Lib.frees_in_term; simplified;
2011-04-27 wenzelm 2011-04-27 more uniform Variable.add_frees/add_fixed etc.;
2011-04-26 wenzelm 2011-04-26 structure Cla as defined in FOL;
2011-04-26 wenzelm 2011-04-26 proper antiquotations;
2011-04-26 wenzelm 2011-04-26 tuned;
2011-04-26 wenzelm 2011-04-26 modernized Clasimp setup;
2011-04-26 wenzelm 2011-04-26 simplified Blast setup;
2011-04-26 wenzelm 2011-04-26 clarified auxiliary structure Lexicon.Syntax;
2011-04-26 wenzelm 2011-04-26 simplified/modernized method setup;
2011-04-26 wenzelm 2011-04-26 simplified/modernized method setup;
2011-04-26 wenzelm 2011-04-26 mark thm tag "kind" as legacy;
2011-04-26 krauss 2011-04-26 mutabelle reports: parse results out of log file
2011-04-23 wenzelm 2011-04-23 hardwired mapping "_" -> "Pure.asm_rl" avoids legacy binding;
2011-04-23 wenzelm 2011-04-23 more precise error positions;
2011-04-23 wenzelm 2011-04-23 clarified Consts.read_const;
2011-04-23 wenzelm 2011-04-23 clarified Type.the_decl;
2011-04-23 wenzelm 2011-04-23 more reports and error positions;
2011-04-23 wenzelm 2011-04-23 added Name_Space.check/get convenience;
2011-04-23 wenzelm 2011-04-23 clarified check_simproc (with report) vs. the_simproc; proper report for @{simproc} (NB: ML environment is built in invisible context); only one data slot for this module;
2011-04-23 wenzelm 2011-04-23 proper binding/report of defined simprocs; tuned signature;
2011-04-23 wenzelm 2011-04-23 modernized specifications;
2011-04-22 wenzelm 2011-04-22 tuned signature;
2011-04-22 wenzelm 2011-04-22 stats for mac-poly-M2;
2011-04-22 wenzelm 2011-04-22 simplified Data signature;
2011-04-22 wenzelm 2011-04-22 misc tuning and simplification;
2011-04-22 wenzelm 2011-04-22 misc tuning;
2011-04-22 wenzelm 2011-04-22 do not open ML structures;
2011-04-22 wenzelm 2011-04-22 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61); tuned signature;
2011-04-22 wenzelm 2011-04-22 modernized Quantifier1 simproc setup;
2011-04-22 wenzelm 2011-04-22 tuned signature;
2011-04-22 wenzelm 2011-04-22 clarified simpset setup; discontinued unused old-style FOL_css;
2011-04-22 blanchet 2011-04-22 iterate the unsound-fact-set removal process to recover even more unsound proofs