2006-04-26 kleing 2006-04-26 added Ben Porter's stuff
2006-04-26 kleing 2006-04-26 moved arithmetic series to geometric series in SetInterval
2006-04-25 wenzelm 2006-04-25 Sign.arity_sorts; tuned;
2006-04-25 wenzelm 2006-04-25 unlocalize_mixfix: fallback on NoSyn;
2006-04-25 wenzelm 2006-04-25 tuned;
2006-04-25 wenzelm 2006-04-25 refer to structure Type instead of Sorts;
2006-04-25 wenzelm 2006-04-25 added inter_sort; added arity_number/sorts;
2006-04-25 wenzelm 2006-04-25 added remove_sort;
2006-04-25 wenzelm 2006-04-25 added arity_number/sorts; tuned;
2006-04-25 wenzelm 2006-04-25 made 'flat' pervasive (again);
2006-04-25 wenzelm 2006-04-25 get_info: removed 'super' field; added params_of, all_params_of; removed params_of_sort; tuned;
2006-04-24 haftmann 2006-04-24 seperated typedef codegen from main code
2006-04-24 haftmann 2006-04-24 more precise tactics
2006-04-24 haftmann 2006-04-24 fixed typo
2006-04-24 haftmann 2006-04-24 more precise data structure
2006-04-24 haftmann 2006-04-24 cleaned up some diagnostic mathom
2006-04-24 haftmann 2006-04-24 moved coalesce to AList, added equality predicates to library
2006-04-23 obua 2006-04-23 added LP.thy
2006-04-22 mengj 2006-04-22 Changed the treatment of equalities.
2006-04-20 mengj 2006-04-20 Changed the logic detection method.
2006-04-19 paulson 2006-04-19 exported linkup_logic_mode and changed the default setting
2006-04-19 paulson 2006-04-19 fix to spacing in switches, for Vampire under SML/NJ
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;