wenzelm [Tue, 21 Jun 2005 09:35:30 +0200] rev 16510
tuned SUBGOAL: Logic.nth_prem instead of List.nth o prems_of;
wenzelm [Tue, 21 Jun 2005 09:31:57 +0200] rev 16509
fixed HOL-Complex-Matrix target;
haftmann [Tue, 21 Jun 2005 08:16:03 +0200] rev 16508
removed mkcontent from makedist
kleing [Tue, 21 Jun 2005 00:45:56 +0200] rev 16507
fix 'give up waiting message' (logs of running processes are not attached)
wenzelm [Mon, 20 Jun 2005 22:14:21 +0200] rev 16506
* Pure: get_thm interface expects datatype thmref;
* More efficient treatment of intermediate theory checkpoints;
wenzelm [Mon, 20 Jun 2005 22:14:20 +0200] rev 16505
avoid identifier 'Name';
wenzelm [Mon, 20 Jun 2005 22:14:19 +0200] rev 16504
Theory.begin/end_theory;
wenzelm [Mon, 20 Jun 2005 22:14:18 +0200] rev 16503
clarify empty vs. pure browser info;
wenzelm [Mon, 20 Jun 2005 22:14:17 +0200] rev 16502
added pointer_eq;
wenzelm [Mon, 20 Jun 2005 22:14:15 +0200] rev 16501
thmref: Name vs. NameSelection;
tuned;
wenzelm [Mon, 20 Jun 2005 22:14:14 +0200] rev 16500
refl_tac: avoid failure of unification, i.e. confusing trace msg;
get_thm(s): Name;
wenzelm [Mon, 20 Jun 2005 22:14:13 +0200] rev 16499
print_theorems: proper use of PureThy.print_theorems_diff;
wenzelm [Mon, 20 Jun 2005 22:14:12 +0200] rev 16498
thmref: Name vs. NameSelection;
wenzelm [Mon, 20 Jun 2005 22:14:11 +0200] rev 16497
generalized type of inter;
added substract;
economize heap usage;
wenzelm [Mon, 20 Jun 2005 22:14:10 +0200] rev 16496
added previous;
wenzelm [Mon, 20 Jun 2005 22:14:09 +0200] rev 16495
added begin_theory, end_theory;
wenzelm [Mon, 20 Jun 2005 22:14:08 +0200] rev 16494
added certify_prop, cert_term, cert_prop;
wenzelm [Mon, 20 Jun 2005 22:14:07 +0200] rev 16493
datatype thmref = Name ... | NameSelection ...;
added print_theorems_diff;
tuned;
wenzelm [Mon, 20 Jun 2005 22:14:06 +0200] rev 16492
added member, option_ord;
wenzelm [Mon, 20 Jun 2005 22:14:05 +0200] rev 16491
OrdList.inter;
wenzelm [Mon, 20 Jun 2005 22:14:04 +0200] rev 16490
tuned;
wenzelm [Mon, 20 Jun 2005 22:14:03 +0200] rev 16489
improved treatment of intermediate checkpoints: actual copy
instead of extend, purge after end;
tuned;
wenzelm [Mon, 20 Jun 2005 22:14:02 +0200] rev 16488
added add_fixrec_i, add_fixpat_i;
ThyParse obsolete;
Sign.read_prop, Sign.cert_prop;
wenzelm [Mon, 20 Jun 2005 22:14:01 +0200] rev 16487
proper header;
wenzelm [Mon, 20 Jun 2005 22:13:59 +0200] rev 16486
get_thm(s): Name;
wenzelm [Mon, 20 Jun 2005 22:13:58 +0200] rev 16485
get_thm instead of obsolete Goals.get_thm;
improved msg;
wenzelm [Mon, 20 Jun 2005 22:13:57 +0200] rev 16484
HOL-Matrix: plain session;
wenzelm [Mon, 20 Jun 2005 22:13:56 +0200] rev 16483
removed obsolete print_depth;
wenzelm [Mon, 20 Jun 2005 22:13:55 +0200] rev 16482
be less ambitious about the author's name;
tuned generated root.tex;
wenzelm [Mon, 20 Jun 2005 22:13:53 +0200] rev 16481
exclude pghead.pdf from doc;
wenzelm [Mon, 20 Jun 2005 21:34:31 +0200] rev 16480
improved formatting;
wenzelm [Mon, 20 Jun 2005 21:33:27 +0200] rev 16479
use Tools/ATP/VampCommunication.ML;
quigley [Mon, 20 Jun 2005 18:39:24 +0200] rev 16478
Added VampCommunication.ML.
Changed small set of Spass rules to Ordered version.
Fixed printing out of resolution proofs if parsing/translation fails.
wenzelm [Mon, 20 Jun 2005 16:41:47 +0200] rev 16477
moved configure to lib/scripts;
wenzelm [Mon, 20 Jun 2005 16:41:20 +0200] rev 16476
./configure obsolete on virtually all systems, but apt to cause problems;
paulson [Mon, 20 Jun 2005 15:55:44 +0200] rev 16475
using TPTP2X_HOME; indentation, etc
paulson [Mon, 20 Jun 2005 15:54:39 +0200] rev 16474
fixed a faulty proof
paulson [Mon, 20 Jun 2005 15:54:22 +0200] rev 16473
moving some generic inequalities from integer arith to nat arith
haftmann [Mon, 20 Jun 2005 11:45:40 +0200] rev 16472
(moved to Distribution/lib/scripts)
haftmann [Mon, 20 Jun 2005 11:30:44 +0200] rev 16471
added fixheaders
wenzelm [Sun, 19 Jun 2005 00:07:41 +0200] rev 16470
improved comment;
wenzelm [Sun, 19 Jun 2005 00:02:06 +0200] rev 16469
some minor adaptions to make it work again;
wenzelm [Sat, 18 Jun 2005 22:57:23 +0200] rev 16468
tuned;
wenzelm [Sat, 18 Jun 2005 22:47:44 +0200] rev 16467
tuned remove;
wenzelm [Sat, 18 Jun 2005 22:42:01 +0200] rev 16466
added member;
wenzelm [Sat, 18 Jun 2005 22:41:18 +0200] rev 16465
added Pure/General/ord_list.ML;
wenzelm [Sat, 18 Jun 2005 22:40:51 +0200] rev 16464
Ordered lists without duplicates.
huffman [Sat, 18 Jun 2005 00:38:18 +0200] rev 16463
fixrec shows unsolved subgoals when proofs of rewrites fail
huffman [Sat, 18 Jun 2005 00:33:27 +0200] rev 16462
make match_rews into simp rules by default
huffman [Fri, 17 Jun 2005 21:19:31 +0200] rev 16461
support theorem names and attributes for fixrec equations; also make them into simp rules by default, like primrec does
huffman [Fri, 17 Jun 2005 18:50:40 +0200] rev 16460
added match functions for ONE, TT, and FF; added theorem mplus_fail2
wenzelm [Fri, 17 Jun 2005 18:36:25 +0200] rev 16459
updated;
wenzelm [Fri, 17 Jun 2005 18:35:27 +0200] rev 16458
accomodate change of TheoryDataFun;
accomodate identification of type Sign.sg and theory;
wenzelm [Fri, 17 Jun 2005 18:33:42 +0200] rev 16457
Context.names_of;
wenzelm [Fri, 17 Jun 2005 18:33:41 +0200] rev 16456
* Pure/TheoryDataFun: change of the argument structure;
* Pure/TheoryDataFun: change of the argument structure -- got rid of Sign.sg;
wenzelm [Fri, 17 Jun 2005 18:33:40 +0200] rev 16455
Sign.root_path, Sign.local_path;
wenzelm [Fri, 17 Jun 2005 18:33:39 +0200] rev 16454
removed obsolete theory_of_sign, theory_of_thm;
Context.draftN;
Context.begin_theory;
wenzelm [Fri, 17 Jun 2005 18:33:38 +0200] rev 16453
PolyML.Compiler.printInAlphabeticalOrder := false;
wenzelm [Fri, 17 Jun 2005 18:33:37 +0200] rev 16452
Context.DATA_FAIL;
accomodate identification of type Sign.sg and theory;
wenzelm [Fri, 17 Jun 2005 18:33:36 +0200] rev 16451
Context.PureN;