2005-06-22 wenzelm 2005-06-22 tuned pointer_eq;
2005-06-22 wenzelm 2005-06-22 renamed data kind;
2005-06-22 wenzelm 2005-06-22 removed proof data (see Pure/context.ML);
2005-06-22 wenzelm 2005-06-22 added depth_of;
2005-06-22 wenzelm 2005-06-22 removed obsolete object.ML (see Pure/library.ML);
2005-06-22 wenzelm 2005-06-22 export sort_ord; tuned term_ord, typ_ord: use pointer_eq; tuned aconv, aconvs: based on term_ord;
2005-06-22 wenzelm 2005-06-22 renamed init to init_data;
2005-06-22 wenzelm 2005-06-22 added structure Object (from Pure/General/object.ML);
2005-06-22 wenzelm 2005-06-22 tuned;
2005-06-22 wenzelm 2005-06-22 begin_thy: merge maximal imports; incorporate proof data; added generic context;
2005-06-22 wenzelm 2005-06-22 removed Pure/Isar/proof_data.ML, Pure/General/object.ML;
2005-06-22 wenzelm 2005-06-22 improved proof;
2005-06-22 wenzelm 2005-06-22 obsolete (see Pure/context.ML);
2005-06-22 wenzelm 2005-06-22 tuned;
2005-06-22 paulson 2005-06-22 pointer equality for sml/nj
2005-06-22 haftmann 2005-06-22 (initial commit)
2005-06-22 haftmann 2005-06-22 (initial commit)
2005-06-22 haftmann 2005-06-22 (initial commit)
2005-06-22 haftmann 2005-06-22 (initial commit)
2005-06-22 nipkow 2005-06-22 *** empty log message ***
2005-06-22 nipkow 2005-06-22 tuned
2005-06-22 nipkow 2005-06-22 added -H false
2005-06-21 quigley 2005-06-21 Integrated vampire lemma code.
2005-06-21 nipkow 2005-06-21 *** empty log message ***
2005-06-21 nipkow 2005-06-21 added find thms section
2005-06-21 wenzelm 2005-06-21 proper implementation of pointer_eq;
2005-06-21 wenzelm 2005-06-21 tuned pointer_eq;
2005-06-21 paulson 2005-06-21 VAMPIRE_HOME, helper_path and various stylistic tweaks
2005-06-21 kleing 2005-06-21 lemma, equation between rtrancl and trancl
2005-06-21 wenzelm 2005-06-21 enter_thms: use theorem database of thy *after* attribute application;
2005-06-21 wenzelm 2005-06-21 tuned;
2005-06-21 wenzelm 2005-06-21 added subset, eq_set; tuned insert/remove: avoid garbage;
2005-06-21 wenzelm 2005-06-21 tuned SUBGOAL: Logic.nth_prem instead of List.nth o prems_of;
2005-06-21 wenzelm 2005-06-21 fixed HOL-Complex-Matrix target;
2005-06-21 haftmann 2005-06-21 removed mkcontent from makedist
2005-06-21 kleing 2005-06-21 fix 'give up waiting message' (logs of running processes are not attached)
2005-06-20 wenzelm 2005-06-20 * Pure: get_thm interface expects datatype thmref; * More efficient treatment of intermediate theory checkpoints;
2005-06-20 wenzelm 2005-06-20 avoid identifier 'Name';
2005-06-20 wenzelm 2005-06-20 Theory.begin/end_theory;
2005-06-20 wenzelm 2005-06-20 clarify empty vs. pure browser info;
2005-06-20 wenzelm 2005-06-20 added pointer_eq;
2005-06-20 wenzelm 2005-06-20 thmref: Name vs. NameSelection; tuned;
2005-06-20 wenzelm 2005-06-20 refl_tac: avoid failure of unification, i.e. confusing trace msg; get_thm(s): Name;
2005-06-20 wenzelm 2005-06-20 print_theorems: proper use of PureThy.print_theorems_diff;
2005-06-20 wenzelm 2005-06-20 thmref: Name vs. NameSelection;
2005-06-20 wenzelm 2005-06-20 generalized type of inter; added substract; economize heap usage;
2005-06-20 wenzelm 2005-06-20 added previous;
2005-06-20 wenzelm 2005-06-20 added begin_theory, end_theory;
2005-06-20 wenzelm 2005-06-20 added certify_prop, cert_term, cert_prop;
2005-06-20 wenzelm 2005-06-20 datatype thmref = Name ... | NameSelection ...; added print_theorems_diff; tuned;
2005-06-20 wenzelm 2005-06-20 added member, option_ord;
2005-06-20 wenzelm 2005-06-20 OrdList.inter;
2005-06-20 wenzelm 2005-06-20 tuned;
2005-06-20 wenzelm 2005-06-20 improved treatment of intermediate checkpoints: actual copy instead of extend, purge after end; tuned;
2005-06-20 wenzelm 2005-06-20 added add_fixrec_i, add_fixpat_i; ThyParse obsolete; Sign.read_prop, Sign.cert_prop;
2005-06-20 wenzelm 2005-06-20 proper header;
2005-06-20 wenzelm 2005-06-20 get_thm(s): Name;
2005-06-20 wenzelm 2005-06-20 get_thm instead of obsolete Goals.get_thm; improved msg;
2005-06-20 wenzelm 2005-06-20 HOL-Matrix: plain session;
2005-06-20 wenzelm 2005-06-20 removed obsolete print_depth;