2011-04-08 wenzelm 2011-04-08 removed outdated text (cf. 84a3f86441eb);
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2011-04-08 wenzelm 2011-04-08 tuned presentation;
2011-04-07 wenzelm 2011-04-07 report literal tokens according to parsetree head; some attempts to stack parsetrees in proper order;
2011-04-07 wenzelm 2011-04-07 simplified read_term vs. read_prop;
2011-04-07 wenzelm 2011-04-07 tuned signature;
2011-04-07 wenzelm 2011-04-07 constant =?= no longer exists (cf. 8c09e1fa24a7);
2011-04-07 wenzelm 2011-04-07 clarified sources -- removed odd comments;
2011-04-07 wenzelm 2011-04-07 tuned signature;
2011-04-07 wenzelm 2011-04-07 merged
2011-04-07 bulwahn 2011-04-07 removing decrement of cardinality in quickcheck -- counting cardinalities starts at 1
2011-04-07 bulwahn 2011-04-07 removing instantiation exhaustive for unit in Quickcheck_Exhaustive
2011-04-07 bulwahn 2011-04-07 correcting bounded_forall construction; tuned
2011-04-07 haftmann 2011-04-07 dropped unused lemmas; proper Isar proof
2011-04-07 blanchet 2011-04-07 further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
2011-04-07 blanchet 2011-04-07 make new Skolemizer more robust
2011-04-07 blanchet 2011-04-07 tuned comment
2011-04-07 wenzelm 2011-04-07 discontinued user-defined token translations; tuned signature;
2011-04-07 wenzelm 2011-04-07 simplified printer context: uniform externing and static token translations;
2011-04-07 wenzelm 2011-04-07 clarified Pretty.mark; added Pretty.mark_str, Pretty.marks_str convenience;
2011-04-06 wenzelm 2011-04-06 parallel parsing of big specifications;
2011-04-06 wenzelm 2011-04-06 separate structure Term_Position; dismantled remains of structure Type_Ext;
2011-04-06 wenzelm 2011-04-06 type syntax as regular mixfix specification (type_ext for bootstrapping has been obsolete for many years);
2011-04-06 wenzelm 2011-04-06 moved type syntax translations to syn_trans.ML;
2011-04-06 wenzelm 2011-04-06 made SML/NJ happy (cf. 578a51fae383);
2011-04-06 wenzelm 2011-04-06 merged
2011-04-06 bulwahn 2011-04-06 merged
2011-04-06 bulwahn 2011-04-06 changing ensure_sort_datatype call in narrowing quickcheck (missed in 1491b7209e76)
2011-04-05 hoelzl 2011-04-05 prove measurable_into_infprod_algebra and measure_infprod
2011-04-05 hoelzl 2011-04-05 Rename extensional to extensionalD (extensional is also defined in FuncSet)
2011-04-06 wenzelm 2011-04-06 eliminated slightly odd Syntax.rep_syntax;
2011-04-06 wenzelm 2011-04-06 more abstract print translation;
2011-04-06 wenzelm 2011-04-06 more abstract syntax translation;
2011-04-06 wenzelm 2011-04-06 tuned;
2011-04-06 wenzelm 2011-04-06 explicit Syntax.tokenize, Syntax.parse;
2011-04-06 wenzelm 2011-04-06 eliminated odd object-oriented type_context/term_context; export ProofContext.intern_skolem;
2011-04-06 wenzelm 2011-04-06 simplified standard parse/unparse;
2011-04-06 wenzelm 2011-04-06 discontinued old-style Syntax.constrainC;
2011-04-06 wenzelm 2011-04-06 typed_print_translation: discontinued show_sorts argument;
2011-04-06 wenzelm 2011-04-06 misc tuning and simplification;
2011-04-06 wenzelm 2011-04-06 moved unparse material to syntax_phases.ML;
2011-04-06 wenzelm 2011-04-06 more symbol abbrevs;
2011-04-06 wenzelm 2011-04-06 renamed Standard_Syntax to Syntax_Phases;
2011-04-05 wenzelm 2011-04-05 moved decode/parse operations to standard_syntax.ML; tuned;
2011-04-05 wenzelm 2011-04-05 separate module for standard implementation of inner syntax operations;
2011-04-05 wenzelm 2011-04-05 moved Isar/local_syntax.ML to Syntax/local_syntax.ML;
2011-04-05 wenzelm 2011-04-05 merged
2011-04-05 blanchet 2011-04-05 added "no_atp" to Cantor's paradox
2011-04-05 blanchet 2011-04-05 renamed "const_args" option value to "args"
2011-04-05 blanchet 2011-04-05 temporarily allow useless encoding of helper facts (e.g. fequal_def) instead of throwing exception
2011-04-05 blanchet 2011-04-05 updated instructions
2011-04-05 blanchet 2011-04-05 minor doc edits
2011-04-05 blanchet 2011-04-05 killed unimplemented type encoding "preds"
2011-04-05 blanchet 2011-04-05 remove debugging code
2011-04-05 bulwahn 2011-04-05 removing bounded_forall code equation for characters when loading Code_Char
2011-04-05 bulwahn 2011-04-05 deriving bounded_forall instances in quickcheck_exhaustive
2011-04-05 bulwahn 2011-04-05 generalizing ensure_sort_datatype for bounded_forall instances
2011-04-04 blanchet 2011-04-04 document "type_sys" option
2011-04-04 blanchet 2011-04-04 if "monomorphize" is enabled, mangle the type information in the names by default
2011-04-05 wenzelm 2011-04-05 use standard tables with standard argument order;