Tue, 28 Sep 1999 15:12:27 +0200 paulson zero_is_mult, by symmetry
Tue, 28 Sep 1999 14:24:22 +0200 wenzelm added W_correct -- correctness of Milner's type inference algorithm W
Tue, 28 Sep 1999 14:15:57 +0200 nipkow documented type solver
Tue, 28 Sep 1999 13:57:33 +0200 nipkow incompatibility solver
Tue, 28 Sep 1999 13:37:54 +0200 paulson more tidying
Mon, 27 Sep 1999 10:25:10 +0200 paulson removed order-sorted theorems from the default claset
Sun, 26 Sep 1999 16:46:25 +0200 wenzelm added 'thms_containing', 'ML_setup';
Sun, 26 Sep 1999 16:45:00 +0200 wenzelm added print_thms_containing;
Sun, 26 Sep 1999 16:44:03 +0200 wenzelm use_mltext: Context.setmp only;
Sun, 26 Sep 1999 16:42:14 +0200 wenzelm help: unknown theory context;
Sun, 26 Sep 1999 16:41:16 +0200 wenzelm added keep', theory';
Sun, 26 Sep 1999 16:39:54 +0200 wenzelm help: unkown theory context;
Sun, 26 Sep 1999 16:38:50 +0200 wenzelm ThmDatabase.print_thms_containing;
Sun, 26 Sep 1999 16:38:21 +0200 wenzelm added print_thms_containing;
Sat, 25 Sep 1999 13:25:16 +0200 wenzelm defs: axmdecl;
Sat, 25 Sep 1999 13:23:58 +0200 wenzelm simplified sectioned_args;
Sat, 25 Sep 1999 13:20:12 +0200 wenzelm added reset_thms;
Sat, 25 Sep 1999 13:19:33 +0200 wenzelm added reset_thms;
Sat, 25 Sep 1999 13:18:38 +0200 wenzelm tuned;
Sat, 25 Sep 1999 13:18:20 +0200 wenzelm defs: name mandatory;
Sat, 25 Sep 1999 13:17:38 +0200 wenzelm avoid interrupts of read loop;
Sat, 25 Sep 1999 13:08:54 +0200 wenzelm simplified sectioned_args;
Sat, 25 Sep 1999 13:08:08 +0200 wenzelm Proof.reset_thms calculationN;
Sat, 25 Sep 1999 13:07:48 +0200 wenzelm admit unbinding;
Sat, 25 Sep 1999 13:06:59 +0200 wenzelm unfold / fold defs;
Sat, 25 Sep 1999 13:06:06 +0200 wenzelm skolem_tag;
Sat, 25 Sep 1999 13:05:38 +0200 wenzelm added fold_rule;
Fri, 24 Sep 1999 17:18:51 +0200 wenzelm * HOL/Real/HahnBanach: the Hahn-Banach theorem for real vector spaces
Fri, 24 Sep 1999 16:33:57 +0200 paulson working version with co-guarantees-leadsto results
Fri, 24 Sep 1999 15:28:12 +0200 wenzelm tuned;
Fri, 24 Sep 1999 12:22:59 +0200 wenzelm tuned;
Fri, 24 Sep 1999 12:22:49 +0200 wenzelm qed "";
Thu, 23 Sep 1999 19:22:52 +0200 wenzelm tuned print_result;
Thu, 23 Sep 1999 18:42:28 +0200 wenzelm improved cycle error;
Thu, 23 Sep 1999 18:39:05 +0200 paulson Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
Thu, 23 Sep 1999 14:39:39 +0200 nipkow sep1 -> sep
Thu, 23 Sep 1999 13:09:39 +0200 paulson The restrict_to_left rule fixes some bugs
Thu, 23 Sep 1999 13:07:25 +0200 paulson Sets new component "restrict_to_left"
Thu, 23 Sep 1999 13:06:31 +0200 paulson tidied; added lemma restrict_to_left
Thu, 23 Sep 1999 09:05:44 +0200 nipkow Restructured lin.arith.package and fixed a proof in RComplete.
Thu, 23 Sep 1999 09:04:36 +0200 nipkow Restructured lin.arith.package.
Wed, 22 Sep 1999 21:49:37 +0200 wenzelm thms_containing: single writeln;
Wed, 22 Sep 1999 21:45:35 +0200 wenzelm tuned pretty_thms;
Wed, 22 Sep 1999 21:45:05 +0200 wenzelm added thms_containing;
Wed, 22 Sep 1999 21:04:55 +0200 wenzelm qed "";
Wed, 22 Sep 1999 21:04:34 +0200 wenzelm proper theory setup for Real/ex/BinEx;
Wed, 22 Sep 1999 21:02:59 +0200 wenzelm tuned;
Wed, 22 Sep 1999 21:02:32 +0200 wenzelm improved output;
Wed, 22 Sep 1999 20:59:22 +0200 wenzelm added 'insert' method (again);
Wed, 22 Sep 1999 20:58:23 +0200 wenzelm ml_store_thm: no warning for "";
Wed, 22 Sep 1999 20:57:51 +0200 wenzelm present results;
Tue, 21 Sep 1999 23:06:50 +0200 wenzelm merged in lost update;
Tue, 21 Sep 1999 19:11:07 +0200 nipkow Mod because of new solver interface.
Tue, 21 Sep 1999 19:10:39 +0200 nipkow ?
Tue, 21 Sep 1999 19:05:38 +0200 nipkow Solvers are now named and stamped.
Tue, 21 Sep 1999 18:11:08 +0200 wenzelm fixed unfold of facts;
Tue, 21 Sep 1999 17:31:20 +0200 wenzelm accomodate refined facts handling;
Tue, 21 Sep 1999 17:30:55 +0200 wenzelm accomodate refined facts handling;
Tue, 21 Sep 1999 17:30:11 +0200 wenzelm Main;
Tue, 21 Sep 1999 17:29:46 +0200 wenzelm Thm.no_prems;
(0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip