2006-04-19 paulson 2006-04-19 definition expansion checks for excess variables
2006-04-19 paulson 2006-04-19 the "th" field of type "clause"
2006-04-19 paulson 2006-04-19 tidying and reformatting
2006-04-19 paulson 2006-04-19 tidying; ATP options including CASC mode for Vampire
2006-04-18 mengj 2006-04-18 Take conjectures and axioms as thms when convert them to ResHolClause.clause format.
2006-04-18 mengj 2006-04-18 Take conjectures and axioms as thms when convert them to ResClause.clause format.
2006-04-18 mengj 2006-04-18 Tidied up some programs.
2006-04-16 haftmann 2006-04-16 fixed typo
2006-04-13 huffman 2006-04-13 add lemma less_UU_iff as default simp rule
2006-04-13 huffman 2006-04-13 hide common name of constant 'run'
2006-04-13 wenzelm 2006-04-13 early test of Classpackage, Codegenerator;
2006-04-13 wenzelm 2006-04-13 fixed typo in method invocation;
2006-04-13 wenzelm 2006-04-13 ignore sort constraints of consts declarations; use conjunction stuff from conjunction.ML; prefer ProofContext.pretty_thm;
2006-04-13 wenzelm 2006-04-13 ignore sort constraints of consts declarations; Sign.typ_equiv;
2006-04-13 wenzelm 2006-04-13 add_axclass(_i): canonical specification format;
2006-04-13 wenzelm 2006-04-13 certify: ignore sort constraints of declarations (MAJOR CHANGE);
2006-04-13 wenzelm 2006-04-13 added print_theorems/theory, print_theorems_diff (from pure_thy.ML);
2006-04-13 wenzelm 2006-04-13 axclass: old-style concrete syntax for canonical specification format;
2006-04-13 wenzelm 2006-04-13 ProofDisplay.print_theorems/theory;
2006-04-13 wenzelm 2006-04-13 added maxidx_of;
2006-04-13 wenzelm 2006-04-13 tuned;
2006-04-13 wenzelm 2006-04-13 added typ_equiv; read_class: improved error;
2006-04-13 wenzelm 2006-04-13 moved print_theorems/theory to Isar/proof_display.ML;
2006-04-13 wenzelm 2006-04-13 added dest_conjunction_list; close_form: canonical order of variables;
2006-04-13 wenzelm 2006-04-13 export unflat (again);
2006-04-13 wenzelm 2006-04-13 use conjunction stuff from conjunction.ML;
2006-04-13 wenzelm 2006-04-13 expand_atom: Type.raw_match;
2006-04-13 wenzelm 2006-04-13 added equal_elim_rule2; export dest_binop; export store_thm etc; moved conjunction stuff to conjunction.ML;
2006-04-13 wenzelm 2006-04-13 tuned comment;
2006-04-13 wenzelm 2006-04-13 ignore sorts of consts declarations;
2006-04-13 wenzelm 2006-04-13 reworded add_axclass(_i): canonical specification format, purely definitional version, always qualify intro/axioms;
2006-04-13 wenzelm 2006-04-13 added conjunction.ML;
2006-04-13 wenzelm 2006-04-13 Meta-level conjunction.
2006-04-13 wenzelm 2006-04-13 added conjunction.ML; tuned;
2006-04-13 wenzelm 2006-04-13 Sign.typ_equiv;
2006-04-13 haftmann 2006-04-13 added subversion treatment
2006-04-11 wenzelm 2006-04-11 classes: prefer thy operations; accomodate tuned interfaces of Logic/Sign/AxClass;
2006-04-11 wenzelm 2006-04-11 export pretty_classrel/arity;
2006-04-11 wenzelm 2006-04-11 'axclass': no parameters;
2006-04-11 wenzelm 2006-04-11 tuned;
2006-04-11 wenzelm 2006-04-11 removed superclasses (see sign.ML);
2006-04-11 wenzelm 2006-04-11 added super_classes (from sorts.ML); removed read/cert_classrel (see axclass.ML);
2006-04-11 wenzelm 2006-04-11 added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML); tuned;
2006-04-11 wenzelm 2006-04-11 moved abstract syntax operations to logic.ML; maintain class parameters; added params_of_sort; added cert/read_classrel (from sign.ML), check class parameters; tuned;
2006-04-10 obua 2006-04-10 Moved stuff from Ring_and_Field to Matrix
2006-04-10 berghofe 2006-04-10 Adapted to changed type of add_typedef_i.
2006-04-10 nipkow 2006-04-10 Hoare(Parallel) dependencies on document/*
2006-04-10 nipkow 2006-04-10 added references
2006-04-10 nipkow 2006-04-10 Minimal doc
2006-04-10 nipkow 2006-04-10 Included cyclic list examples
2006-04-10 haftmann 2006-04-10 fixed value restriction
2006-04-10 nipkow 2006-04-10 Added splicing algorithm.
2006-04-10 wenzelm 2006-04-10 hide (open) const;
2006-04-10 wenzelm 2006-04-10 simplified AxClass.add_axclass interface;
2006-04-10 wenzelm 2006-04-10 added aT (from axclass.ML); non-pervasive itselfT, a_itselfT;
2006-04-10 wenzelm 2006-04-10 removed unused class_le_path, sort_less;
2006-04-10 wenzelm 2006-04-10 add_axclass(_i): return class name only; subclass/arity statements: require actual TVars, store raw data; tuned;
2006-04-10 wenzelm 2006-04-10 Term.itselfT;
2006-04-09 nipkow 2006-04-09 Added function "splice"
2006-04-09 wenzelm 2006-04-09 Even/Odd: avoid clash with even/odd of Main HOL;