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
2008-06-20 huffman 2008-06-20 added some lemmas; tuned proofs
2008-06-20 huffman 2008-06-20 tuned
2008-06-20 huffman 2008-06-20 replace less_lift with flat_less_iff
2008-06-20 huffman 2008-06-20 tweak lemmas adm_all and adm_ball
2008-06-19 huffman 2008-06-19 move lemmas into locales; restructure some proofs
2008-06-19 huffman 2008-06-19 add lemmas take_chain_less and take_chain_le
2008-06-19 wenzelm 2008-06-19 disposed Sign.read_typ etc;
2008-06-19 wenzelm 2008-06-19 renamed is_abbrev_mode to abbrev_mode; added private get_sort (from sign.ML);
2008-06-19 wenzelm 2008-06-19 ProofContext.abbrev_mode;
2008-06-19 wenzelm 2008-06-19 moved get_sort to Isar/proof_context.ML; removed obsolete read_def_typ, read_typ, read_typ_syntax, read_typ_abbrev;
2008-06-19 wenzelm 2008-06-19 tuned signature; removed duplicates of read_typ/cert_typ (cf. RecordPackage.read_typ/cert_typ);
2008-06-19 wenzelm 2008-06-19 private add_used (from drule.ML); Variable.declare_names;
2008-06-19 wenzelm 2008-06-19 Variable.declare_typ;
2008-06-19 wenzelm 2008-06-19 added declare_typ;
2008-06-19 wenzelm 2008-06-19 moved add_used to Isar/rule_insts.ML;
2008-06-19 wenzelm 2008-06-19 export read_typ/cert_typ -- version with regular context operations; tuned;
2008-06-19 wenzelm 2008-06-19 export read_typ/cert_typ -- version with regular context operations;
2008-06-19 wenzelm 2008-06-19 tuned signature; removed duplicate of RecordPackage.read_typ; replaced Typetab by existing Typtab;
2008-06-19 wenzelm 2008-06-19 removed duplicate of DatatypePackage.read_typ;
2008-06-19 huffman 2008-06-19 add lemma cfcomp_LAM
2008-06-19 wenzelm 2008-06-19 add_abbrev: check tfrees of rhs, not tvars (addresses a lapse introduced in 1.65);
2008-06-19 urbanc 2008-06-19 slightly tuned
2008-06-19 krauss 2008-06-19 generalized induct_scheme method to prove conditional induction schemes.
2008-06-19 huffman 2008-06-19 add lemma iterate_iterate
2008-06-18 wenzelm 2008-06-18 * Disposed old term read functions;
2008-06-18 huffman 2008-06-18 replace preorder class with locale
2008-06-18 huffman 2008-06-18 add lemma compact_imp_principal to locale ideal_completion
2008-06-18 wenzelm 2008-06-18 added type_constraint (formerly in type_infer.ML, which is now loaded later);
2008-06-18 wenzelm 2008-06-18 TypeExt.type_constraint;
2008-06-18 wenzelm 2008-06-18 simplified TypeInfer.infer_types;
2008-06-18 wenzelm 2008-06-18 improved error output -- variant/mark bounds; simplified infer_types -- always freeze, no result substitution;
2008-06-18 wenzelm 2008-06-18 load type_infer.ML after Syntax module;
2008-06-18 wenzelm 2008-06-18 eliminated old Sign.read_term/Thm.read_cterm etc.;
2008-06-18 wenzelm 2008-06-18 moved ProofContext.pretty_proof to ProofSyntax.pretty_proof; read_term: imitate old behaviour (allow_dummies, mode_schematic);
2008-06-18 wenzelm 2008-06-18 export transfer_syntax; added allow_dummies feature (for legacy emulations); moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
2008-06-18 wenzelm 2008-06-18 moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
2008-06-18 wenzelm 2008-06-18 removed obsolete term reading operations (cf. old_goals.ML for legacy emulations);
2008-06-18 wenzelm 2008-06-18 added emulations for simple_read_term/read_term/read_prop (formerly in sign.ML);
2008-06-18 wenzelm 2008-06-18 removed obsolete read_def_cterms/read_cterm;
2008-06-18 wenzelm 2008-06-18 load proof term operations later;
2008-06-18 wenzelm 2008-06-18 more antiquotations;
2008-06-18 wenzelm 2008-06-18 OldGoals.read_prop;
2008-06-18 wenzelm 2008-06-18 OldGoals.simple_read_term;
2008-06-18 wenzelm 2008-06-18 simplified Abel_Cancel setup;
2008-06-18 wenzelm 2008-06-18 updated generated file;
2008-06-18 wenzelm 2008-06-18 pervasive cut_inst_tac;
2008-06-17 urbanc 2008-06-17 added a progress lemma and tuned some comments
2008-06-16 wenzelm 2008-06-16 * Rules and tactics that read instantiations now demand a proper context;
2008-06-16 wenzelm 2008-06-16 added instantiate_tac, cut_inst_tac, forw_inst_tac, dres_inst_tac, make_elim_preserve (from tactic.ML); pervasive operations; tuned;
2008-06-16 wenzelm 2008-06-16 renamed rename_params_tac to rename_tac;
2008-06-16 wenzelm 2008-06-16 removed obsolete global instantiation tactics (cf. Isar/rule_insts.ML); removed obsolete rename_tac, rename_last_tac; renamed rename_params_tac to rename_tac;