Tue, 21 Jun 2005 09:51:59 +0200 wenzelm enter_thms: use theorem database of thy *after* attribute application;
Tue, 21 Jun 2005 09:35:32 +0200 wenzelm tuned;
Tue, 21 Jun 2005 09:35:31 +0200 wenzelm added subset, eq_set;
Tue, 21 Jun 2005 09:35:30 +0200 wenzelm tuned SUBGOAL: Logic.nth_prem instead of List.nth o prems_of;
Tue, 21 Jun 2005 09:31:57 +0200 wenzelm fixed HOL-Complex-Matrix target;
Tue, 21 Jun 2005 08:16:03 +0200 haftmann removed mkcontent from makedist
Tue, 21 Jun 2005 00:45:56 +0200 kleing fix 'give up waiting message' (logs of running processes are not attached)
Mon, 20 Jun 2005 22:14:21 +0200 wenzelm * Pure: get_thm interface expects datatype thmref;
Mon, 20 Jun 2005 22:14:20 +0200 wenzelm avoid identifier 'Name';
Mon, 20 Jun 2005 22:14:19 +0200 wenzelm Theory.begin/end_theory;
Mon, 20 Jun 2005 22:14:18 +0200 wenzelm clarify empty vs. pure browser info;
Mon, 20 Jun 2005 22:14:17 +0200 wenzelm added pointer_eq;
Mon, 20 Jun 2005 22:14:15 +0200 wenzelm thmref: Name vs. NameSelection;
Mon, 20 Jun 2005 22:14:14 +0200 wenzelm refl_tac: avoid failure of unification, i.e. confusing trace msg;
Mon, 20 Jun 2005 22:14:13 +0200 wenzelm print_theorems: proper use of PureThy.print_theorems_diff;
Mon, 20 Jun 2005 22:14:12 +0200 wenzelm thmref: Name vs. NameSelection;
Mon, 20 Jun 2005 22:14:11 +0200 wenzelm generalized type of inter;
Mon, 20 Jun 2005 22:14:10 +0200 wenzelm added previous;
Mon, 20 Jun 2005 22:14:09 +0200 wenzelm added begin_theory, end_theory;
Mon, 20 Jun 2005 22:14:08 +0200 wenzelm added certify_prop, cert_term, cert_prop;
Mon, 20 Jun 2005 22:14:07 +0200 wenzelm datatype thmref = Name ... | NameSelection ...;
Mon, 20 Jun 2005 22:14:06 +0200 wenzelm added member, option_ord;
Mon, 20 Jun 2005 22:14:05 +0200 wenzelm OrdList.inter;
Mon, 20 Jun 2005 22:14:04 +0200 wenzelm tuned;
Mon, 20 Jun 2005 22:14:03 +0200 wenzelm improved treatment of intermediate checkpoints: actual copy
Mon, 20 Jun 2005 22:14:02 +0200 wenzelm added add_fixrec_i, add_fixpat_i;
Mon, 20 Jun 2005 22:14:01 +0200 wenzelm proper header;
Mon, 20 Jun 2005 22:13:59 +0200 wenzelm get_thm(s): Name;
Mon, 20 Jun 2005 22:13:58 +0200 wenzelm get_thm instead of obsolete Goals.get_thm;
Mon, 20 Jun 2005 22:13:57 +0200 wenzelm HOL-Matrix: plain session;
Mon, 20 Jun 2005 22:13:56 +0200 wenzelm removed obsolete print_depth;
Mon, 20 Jun 2005 22:13:55 +0200 wenzelm be less ambitious about the author's name;
Mon, 20 Jun 2005 22:13:53 +0200 wenzelm exclude pghead.pdf from doc;
Mon, 20 Jun 2005 21:34:31 +0200 wenzelm improved formatting;
Mon, 20 Jun 2005 21:33:27 +0200 wenzelm use Tools/ATP/VampCommunication.ML;
Mon, 20 Jun 2005 18:39:24 +0200 quigley Added VampCommunication.ML.
Mon, 20 Jun 2005 16:41:47 +0200 wenzelm moved configure to lib/scripts;
Mon, 20 Jun 2005 16:41:20 +0200 wenzelm ./configure obsolete on virtually all systems, but apt to cause problems;
Mon, 20 Jun 2005 15:55:44 +0200 paulson using TPTP2X_HOME; indentation, etc
Mon, 20 Jun 2005 15:54:39 +0200 paulson fixed a faulty proof
Mon, 20 Jun 2005 15:54:22 +0200 paulson moving some generic inequalities from integer arith to nat arith
Mon, 20 Jun 2005 11:45:40 +0200 haftmann (moved to Distribution/lib/scripts)
Mon, 20 Jun 2005 11:30:44 +0200 haftmann added fixheaders
Sun, 19 Jun 2005 00:07:41 +0200 wenzelm improved comment;
Sun, 19 Jun 2005 00:02:06 +0200 wenzelm some minor adaptions to make it work again;
Sat, 18 Jun 2005 22:57:23 +0200 wenzelm tuned;
Sat, 18 Jun 2005 22:47:44 +0200 wenzelm tuned remove;
Sat, 18 Jun 2005 22:42:01 +0200 wenzelm added member;
Sat, 18 Jun 2005 22:41:18 +0200 wenzelm added Pure/General/ord_list.ML;
Sat, 18 Jun 2005 22:40:51 +0200 wenzelm Ordered lists without duplicates.
Sat, 18 Jun 2005 00:38:18 +0200 huffman fixrec shows unsolved subgoals when proofs of rewrites fail
Sat, 18 Jun 2005 00:33:27 +0200 huffman make match_rews into simp rules by default
Fri, 17 Jun 2005 21:19:31 +0200 huffman support theorem names and attributes for fixrec equations; also make them into simp rules by default, like primrec does
Fri, 17 Jun 2005 18:50:40 +0200 huffman added match functions for ONE, TT, and FF; added theorem mplus_fail2
Fri, 17 Jun 2005 18:36:25 +0200 wenzelm updated;
Fri, 17 Jun 2005 18:35:27 +0200 wenzelm accomodate change of TheoryDataFun;
Fri, 17 Jun 2005 18:33:42 +0200 wenzelm Context.names_of;
Fri, 17 Jun 2005 18:33:41 +0200 wenzelm * Pure/TheoryDataFun: change of the argument structure;
Fri, 17 Jun 2005 18:33:40 +0200 wenzelm Sign.root_path, Sign.local_path;
Fri, 17 Jun 2005 18:33:39 +0200 wenzelm removed obsolete theory_of_sign, theory_of_thm;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip