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);
2008-06-21 wenzelm 2008-06-21 the_tags: explicit error message; new_decl: Position.thread_data;
2008-06-21 wenzelm 2008-06-21 activate_context: strict the_context, no fallback on theory context;
2008-06-20 huffman 2008-06-20 remove unused constant liftpair
2008-06-20 huffman 2008-06-20 simplify profinite class axioms
2008-06-20 huffman 2008-06-20 clean up and rename some profinite lemmas
2008-06-20 isatest 2008-06-20 move at-sml-dev-e to macbroy23
2008-06-20 huffman 2008-06-20 replace SetPcpo.thy with Cset.thy
2008-06-20 wenzelm 2008-06-20 updated for 2008; proper name of TUM;
2008-06-20 haftmann 2008-06-20 (removed non-present change)
2008-06-20 haftmann 2008-06-20 explicit thm context for error messages
2008-06-20 haftmann 2008-06-20 using tages to find theory names
2008-06-20 haftmann 2008-06-20 type constructors now with markup
2008-06-20 haftmann 2008-06-20 fixed bind error for malformed primrec specifications
2008-06-20 haftmann 2008-06-20 DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
2008-06-20 haftmann 2008-06-20 streamlined definitions
2008-06-20 haftmann 2008-06-20 moved Float.thy to Library
2008-06-20 huffman 2008-06-20 removed SetPcpo.thy and cpo instance for type bool; added Cset.thy with pcpo type 'a cset isomorphic to 'a set; updated ideal completion theory to use cset
2008-06-20 huffman 2008-06-20 moved Abs_image to Typedef.thy; prove finite_UNIV outside the locale
2008-06-20 huffman 2008-06-20 add lemma Abs_image
2008-06-20 huffman 2008-06-20 added some lemmas; reorganized into sections; tuned proofs