2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-20 mengj 2006-01-20 type information is now also printed.
2006-01-20 mengj 2006-01-20 added some debugging code.
2006-01-20 mengj 2006-01-20 fixed a bug
2006-01-19 wenzelm 2006-01-19 quote "atom";
2006-01-19 wenzelm 2006-01-19 updated;
2006-01-19 wenzelm 2006-01-19 * ML/Isar: theory setup has type (theory -> theory);
2006-01-19 wenzelm 2006-01-19 use/use_thy: Output.toplevel_errors;
2006-01-19 wenzelm 2006-01-19 added basic syntax; removed pure syntax;
2006-01-19 wenzelm 2006-01-19 moved pure syntax to Syntax/syntax.ML and pure_thy.ML;
2006-01-19 wenzelm 2006-01-19 keep: disable Output.toplevel_errors; program: Output.ML_errors;
2006-01-19 wenzelm 2006-01-19 run_thy: removed Output.toplevel_errors;
2006-01-19 wenzelm 2006-01-19 added ML_errors;
2006-01-19 wenzelm 2006-01-19 use: Output.ML_errors;
2006-01-19 wenzelm 2006-01-19 Syntax.basic_syn;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory; added syntax (from Syntax/mixfix.ML); added HTML output syntax for _lambda;
2006-01-19 wenzelm 2006-01-19 tuned setmp;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory; use_output: Output.ML_errors;
2006-01-19 wenzelm 2006-01-19 tuned comments;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory; Syntax.appl(C)_syntax;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-19 berghofe 2006-01-19 Use generic Simplifier.simp_add attribute instead of Simplifier.simp_add_global.
2006-01-19 berghofe 2006-01-19 Re-inserted consts_code declaration accidentally deleted during last commit.
2006-01-19 paulson 2006-01-19 strengthened some lemmas; simplified some proofs
2006-01-18 haftmann 2006-01-18 substantial improvement in serialization handling
2006-01-18 urbanc 2006-01-18 fixed one proof that broke because of the changes Markus did on the rules ex1I
2006-01-17 haftmann 2006-01-17 substantial improvements in code generator
2006-01-17 paulson 2006-01-17 these hacks are no longer needed
2006-01-17 paulson 2006-01-17 improved SPASS support
2006-01-16 wenzelm 2006-01-16 case_result: drop_schematic, i.e. be permissive about illegal binds;
2006-01-16 wenzelm 2006-01-16 put_facts: do not pretend local thms were named;
2006-01-16 wenzelm 2006-01-16 declare the1_equality [elim?];
2006-01-15 wenzelm 2006-01-15 tuned;
2006-01-15 wenzelm 2006-01-15 tuned;
2006-01-15 wenzelm 2006-01-15 * Classical: optional weight for attributes; * HOL: prefer ex1I over ex_ex1I in single-step reasoning;
2006-01-15 wenzelm 2006-01-15 guess: used fixed inferred_type of vars;
2006-01-15 wenzelm 2006-01-15 export add_args; tuned;
2006-01-15 wenzelm 2006-01-15 attributes: optional weight; tuned;
2006-01-15 wenzelm 2006-01-15 classical attributes: optional weight;
2006-01-15 wenzelm 2006-01-15 prefer ex1I over ex_ex1I in single-step reasoning;
2006-01-14 wenzelm 2006-01-14 generic attributes;
2006-01-14 wenzelm 2006-01-14 tuned;
2006-01-14 wenzelm 2006-01-14 * ML/Isar: simplified treatment of user-level errors;
2006-01-14 wenzelm 2006-01-14 sane ERROR vs. TOPLEVEL_ERROR handling; added program;
2006-01-14 wenzelm 2006-01-14 added Isar.toplevel;
2006-01-14 wenzelm 2006-01-14 Output.error_msg;
2006-01-14 wenzelm 2006-01-14 removed special ERROR handling stuff (transform_error etc.); moved plain ERROR/error to library.ML; added toplevel_errors, exception TOPLEVEL_ERROR; error_msg, panic, info, debug no longer pervasive;
2006-01-14 wenzelm 2006-01-14 added exception ERROR, error, cat_error, sys_error, assert, deny, assert_all; added transform_failure; added prefix;
2006-01-14 wenzelm 2006-01-14 Output.debug;
2006-01-14 wenzelm 2006-01-14 generated code: raise Match instead of ERROR;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2006-01-13 paulson 2006-01-13 blacklist experiments
2006-01-13 paulson 2006-01-13 more readable divide ops
2006-01-13 paulson 2006-01-13 more practical time limit
2006-01-13 nipkow 2006-01-13 *** empty log message ***
2006-01-13 wenzelm 2006-01-13 mixfix: added Structure;
2006-01-13 wenzelm 2006-01-13 uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag; mixfix: added Structure; renamed type exporter to export; removed obsolete sign_of; tuned signature; tuned;
2006-01-13 wenzelm 2006-01-13 uniform handling of fixes; mixfix: added Structure; tuned;
2006-01-13 wenzelm 2006-01-13 uniform handling of fixes;
2006-01-13 wenzelm 2006-01-13 uniform handling of fixes; mixfix: added Structure;