2007-10-13 wenzelm 2007-10-13 Theory.specify_const: added deps argument;
2007-10-13 wenzelm 2007-10-13 renamed LocalTheory.def to LocalTheory.define;
2007-10-12 webertj 2007-10-12 typo in comment fixed
2007-10-12 webertj 2007-10-12 significant code overhaul, bugfix for inductive data types
2007-10-12 wenzelm 2007-10-12 added generic provide_file; tuned;
2007-10-12 wenzelm 2007-10-12 pass explicit target record -- more informative peek operation; removed obsolete hide_abbrev; misc tuning;
2007-10-12 wenzelm 2007-10-12 more informative TheoryTarget.peek operation;
2007-10-12 wenzelm 2007-10-12 fork_mixfix: explicit bool argument;
2007-10-12 wenzelm 2007-10-12 eval_term: moved actual evaluation out of CRITICAL section;
2007-10-12 paulson 2007-10-12 preventing eta-redexes in theorems from causing failure
2007-10-12 paulson 2007-10-12 trying to make it run faster
2007-10-12 paulson 2007-10-12 calling the correct interface
2007-10-12 wenzelm 2007-10-12 replaced syntax/translations by abbreviation;
2007-10-12 haftmann 2007-10-12 updated
2007-10-12 haftmann 2007-10-12 dropped local_syntax
2007-10-12 haftmann 2007-10-12 tuned
2007-10-12 haftmann 2007-10-12 (intermediate quickfix)
2007-10-12 haftmann 2007-10-12 removed
2007-10-12 haftmann 2007-10-12 added
2007-10-12 paulson 2007-10-12 metis calls
2007-10-12 haftmann 2007-10-12 updated
2007-10-12 haftmann 2007-10-12 moved class power to theory Power
2007-10-12 haftmann 2007-10-12 refined; moved class power to theory Power
2007-10-12 haftmann 2007-10-12 consolidated naming conventions for code generator theories
2007-10-12 haftmann 2007-10-12 class div inherits from class times
2007-10-12 haftmann 2007-10-12 code_include replaces code_moduleprolog
2007-10-12 haftmann 2007-10-12 added subclass command
2007-10-11 wenzelm 2007-10-11 enabled Refute_Examples again;
2007-10-11 wenzelm 2007-10-11 local_axioms: impose hyps stemming from local consts as well (otherwise the axioms will be more general than expected!);
2007-10-11 wenzelm 2007-10-11 disabled Refute_Examples temporarily;
2007-10-11 wenzelm 2007-10-11 local_theory: incorporated consts into axioms; LocalDefs.expand_cterm; tuned;
2007-10-11 wenzelm 2007-10-11 removed unused/impure quiet_mode; local_theory: incorporated consts into axioms; tuned;
2007-10-11 wenzelm 2007-10-11 added export_cterm; tuned;
2007-10-11 wenzelm 2007-10-11 local_theory: incorporated consts into axioms;
2007-10-11 wenzelm 2007-10-11 replaced Term.equiv_types by Type.similar_types; moved add_axiom/def to more_thm.ML;
2007-10-11 wenzelm 2007-10-11 replaced Term.equiv_types by Type.similar_types;
2007-10-11 wenzelm 2007-10-11 dest/cert_def: replaced Pretty.pp by explicit Proof.context;
2007-10-11 wenzelm 2007-10-11 added elim_implies (more convenient argument order); added unvarify (from drule.ML); added specification primitives: add_axiom, add_def;
2007-10-11 wenzelm 2007-10-11 removed obsolete flip;
2007-10-11 wenzelm 2007-10-11 moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML); tuned;
2007-10-11 wenzelm 2007-10-11 replaced (flip Thm.implies_elim) by Thm.elim_implies;
2007-10-11 wenzelm 2007-10-11 moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML);
2007-10-11 wenzelm 2007-10-11 usedir: added HOL_USEDIR_OPTIONS;
2007-10-11 paulson 2007-10-11 reconstruction bug fix
2007-10-11 wenzelm 2007-10-11 tuned;
2007-10-11 wenzelm 2007-10-11 replaced Sign.add_consts_i by Sign.declare_const;
2007-10-11 wenzelm 2007-10-11 replaced Sign.add_consts_authentic by Sign.declare_const; tuned;
2007-10-11 wenzelm 2007-10-11 renamed Syntax.XXX_mode to Syntax.mode_XXX; moved ProofContext.pp to Syntax.pp;
2007-10-11 wenzelm 2007-10-11 removed obsolete AxClass.params_of_class; tuned;
2007-10-11 wenzelm 2007-10-11 replaced Sign.add_consts_authentic by Sign.declare_const; replaced read_param by Sign.read_const, which is independent of syntax; added define_class_params (from axclass.ML);
2007-10-11 wenzelm 2007-10-11 load axclass.ML before Isar; load subclass.ML earlier;
2007-10-11 wenzelm 2007-10-11 added specify_const;
2007-10-11 wenzelm 2007-10-11 removed obsolete simple_def;
2007-10-11 wenzelm 2007-10-11 moved define_class_params to Isar/class.ML; removed obsolete params_of_class, print_axclasses; moved ProofContext.pp to Syntax.pp; misc tuning;
2007-10-11 wenzelm 2007-10-11 load axclass.ML before Isar;
2007-10-11 wenzelm 2007-10-11 Theory.specify_const;
2007-10-11 wenzelm 2007-10-11 moved ProofContext.pp to Syntax.pp;
2007-10-11 wenzelm 2007-10-11 renamed Syntax.XXX_mode to Syntax.mode_XXX;
2007-10-11 wenzelm 2007-10-11 replaced Sign.add_consts_authentic by Sign.declare_const;
2007-10-11 paulson 2007-10-11 rationalized redundant code