2009-03-23 ago haftmann moved Imperative_HOL examples to Imperative_HOL/ex
2009-03-23 ago haftmann corrected variable renaming
2009-03-23 ago haftmann tuned error messages
2009-03-23 ago haftmann moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
2009-03-23 ago haftmann structure LinArith now named Lin_Arith
2009-03-23 ago haftmann suddenly infix identifier oo occurs in generated code
2009-03-24 ago wenzelm datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
2009-03-24 ago wenzelm eliminated non-canonical alias structure T = ML_Lex;
2009-03-24 ago wenzelm error "Static Errors";
2009-03-24 ago wenzelm more systematic type use_context;
2009-03-23 ago wenzelm tuned;
2009-03-23 ago wenzelm more systematic type use_context;
2009-03-23 ago wenzelm eliminated Output.ml_output;
2009-03-23 ago wenzelm pretty_ml/ml_pretty: proper handling of markup and string length;
2009-03-23 ago wenzelm more systematic type use_context;
2009-03-23 ago wenzelm removed obsolete ml_output;
2009-03-23 ago wenzelm more systematic type use_context;
2009-03-23 ago wenzelm more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
2009-03-23 ago wenzelm de-camelized ML_Name_Space;
2009-03-23 ago wenzelm suppress status output for traditional tty modes (including Proof General);
2009-03-23 ago wenzelm added report_text -- status messages with text body;
2009-03-23 ago wenzelm maintain parse trees cumulatively;
2009-03-23 ago wenzelm Block markup: maintain output version within tree values (in accordance with String) -- changes operational behaviour wrt. print_mode;
2009-03-23 ago wenzelm future scheduler: reduced wait timeout if tasks need to be canceled -- to improve reactivity of interrupts;
2009-03-23 ago haftmann merged
2009-03-23 ago haftmann Main is (Complex_Main) base entry point in library theories
2009-03-23 ago haftmann Main is (Complex_Main) base entry point in library theories
2009-03-23 ago haftmann added instances for bot, top, wellorder
2009-03-23 ago haftmann tuned header
2009-03-23 ago haftmann more canonical import, syntax fix
2009-03-23 ago haftmann merged
2009-03-22 ago haftmann merged
2009-03-22 ago haftmann more antiquotations
2009-03-22 ago haftmann moved import of module qelim to theory Presburger
2009-03-22 ago haftmann tuned header
2009-03-22 ago haftmann dropped theory Arith_Tools
2009-03-22 ago haftmann lemma nat_dvd_not_less moved here from Arith_Tools
2009-03-22 ago haftmann distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
2009-03-22 ago wenzelm merged
2009-03-22 ago nipkow merged
2009-03-22 ago nipkow 1. New cancellation simprocs for common factors in inequations
2009-03-22 ago haftmann clarified relationship of modules Code_Name and Code_Printer
2009-03-22 ago haftmann added Symreltab (binary relations of symbols) instance of TableFun
2009-03-22 ago wenzelm proper signature;
2009-03-22 ago wenzelm added read_antiq, with improved error reporting;
2009-03-22 ago wenzelm ML_Lex.read_antiq;
2009-03-22 ago wenzelm ML_Lex.read_antiq;
2009-03-22 ago wenzelm simplified Antiquote.read (again);
2009-03-22 ago wenzelm export report -- version that actually covers all cases;
2009-03-22 ago wenzelm Test of advanced ML compiler invocation in Poly/ML 5.3.
2009-03-22 ago wenzelm ML/ml_test.ML: test of advanced ML compiler invocation in Poly/ML 5.3;
2009-03-22 ago wenzelm added pretty_ml;
2009-03-22 ago wenzelm export eval_antiquotes: refined version that operates on ML tokens;
2009-03-22 ago wenzelm ML_Lex.pos_of: regular position;
2009-03-22 ago wenzelm replaced Antiquote.is_antiq by Antiquote.is_text;
2009-03-21 ago wenzelm merged
2009-03-21 ago wenzelm extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
2009-03-21 ago wenzelm merged
2009-03-21 ago huffman merged
2009-03-21 ago huffman move field lemmas into class locale context