2008-06-26 huffman 2008-06-26 remove cset theory; define ideal completions using typedef instead of cpodef
2008-06-26 wenzelm 2008-06-26 Args.theory;
2008-06-26 wenzelm 2008-06-26 added context/theory scanner;
2008-06-26 wenzelm 2008-06-26 Args.context;
2008-06-26 krauss 2008-06-26 fix: need to beta/eta normalize
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2008-06-26 haftmann 2008-06-26 added dummy citiation
2008-06-26 haftmann 2008-06-26 dropped recdef
2008-06-26 haftmann 2008-06-26 class theory name lookup improved
2008-06-25 wenzelm 2008-06-25 modernized specifications;
2008-06-25 wenzelm 2008-06-25 tuned proofs;
2008-06-25 wenzelm 2008-06-25 modernized specifications;
2008-06-25 wenzelm 2008-06-25 modernized specifications;
2008-06-25 urbanc 2008-06-25 typo
2008-06-25 wenzelm 2008-06-25 re-use official outer keywords;
2008-06-25 wenzelm 2008-06-25 scan: prefer command over keyword, allowing lexicons to overlap;
2008-06-25 wenzelm 2008-06-25 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces; lexicons: allow overlapping keywords/commands -- warning instead of error;
2008-06-25 wenzelm 2008-06-25 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces; moved check_text here;
2008-06-25 wenzelm 2008-06-25 antiquote: need to quote outer keywords;
2008-06-25 wenzelm 2008-06-25 tuned;
2008-06-25 wenzelm 2008-06-25 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
2008-06-25 berghofe 2008-06-25 - Equivariance simpset used in proofs of strong induction and inversion rules now contains perm_simproc_app and perm_simproc_fun as well - first_order_matchs now eta-contracts terms before matching - Rewrote code for proving strong inversion rule to avoid failure when one of the arguments of the inductive predicate has an atom type
2008-06-25 wenzelm 2008-06-25 pprint: back to proper output of markup, with workaround for Poly/ML crash;
2008-06-24 wenzelm 2008-06-24 back to 1.36 (Poly/ML crash!?);
2008-06-24 wenzelm 2008-06-24 updated generated file;
2008-06-24 wenzelm 2008-06-24 YXML: no special treatment of white space;
2008-06-24 wenzelm 2008-06-24 pprint: proper output of markup (important for token translation);
2008-06-24 wenzelm 2008-06-24 ml_code_antiq: proper scanner combinators; ML_Antiquote.value;
2008-06-24 wenzelm 2008-06-24 moved concrete antiquotations to ml_antiquote.ML;
2008-06-24 wenzelm 2008-06-24 Antiquote.Open/Close;
2008-06-24 wenzelm 2008-06-24 add_antiq: more general notion of ML antiquotation; eval_antiquotes: support blocks and background context; moved concrete antiquotations to ml_antiquote.ML;
2008-06-24 wenzelm 2008-06-24 added Open/Close -- checked blocks;
2008-06-24 wenzelm 2008-06-24 added pprint_thy_ref;
2008-06-24 wenzelm 2008-06-24 Common ML antiquotations.
2008-06-24 wenzelm 2008-06-24 added ML/ml_antiquote.ML;
2008-06-24 wenzelm 2008-06-24 ML_Antiquote.value;
2008-06-24 wenzelm 2008-06-24 added isaantiqopen/close;
2008-06-23 wenzelm 2008-06-23 Logic.all/mk_equals/mk_implies; Term.all;
2008-06-23 wenzelm 2008-06-23 moved implies to logic.ML; removed equals; qualified all;
2008-06-23 wenzelm 2008-06-23 added all, is_all; improved dest_all; added implies (from term.ML);
2008-06-23 wenzelm 2008-06-23 Logic.implies;
2008-06-23 wenzelm 2008-06-23 Logic.is_all;
2008-06-23 wenzelm 2008-06-23 Term.all;
2008-06-23 wenzelm 2008-06-23 Logic.all/mk_equals/mk_implies;
2008-06-23 wenzelm 2008-06-23 session name: empty for Pure and by default;
2008-06-23 wenzelm 2008-06-23 induct_tac: allow omission of arguments;
2008-06-23 wenzelm 2008-06-23 info: default name is "", not "Pure";
2008-06-23 wenzelm 2008-06-23 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
2008-06-23 wenzelm 2008-06-23 removed obsolete dest_concls;
2008-06-23 wenzelm 2008-06-23 induct_tac: mutual rules work as for method "induct";
2008-06-23 wenzelm 2008-06-23 tuned get_inductT: *all* rules for missing instantiation; exported get_inductT;
2008-06-23 wenzelm 2008-06-23 induct_tac: infer mutual rule from types, as for proper induct method;
2008-06-23 wenzelm 2008-06-23 induct_tac/case_tac: nested tuples are split as expected;
2008-06-23 wenzelm 2008-06-23 induct_tac: old conjunctive rules no longer supported;
2008-06-23 wenzelm 2008-06-23 updated generated file;
2008-06-23 wenzelm 2008-06-23 induct_tac: rule is inferred from types;
2008-06-22 huffman 2008-06-22 cleaned up some proofs; removed unused stuff about totally-ordered sets; import Main
2008-06-22 huffman 2008-06-22 use new-style abbreviation/notation for fix syntax
2008-06-21 wenzelm 2008-06-21 import_export_proof: simplified thm definition -- PureThy.name_thm does the job;
2008-06-21 wenzelm 2008-06-21 added query_type/const/class (meta data);