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;
Tue, 21 Sep 1999 17:29:00 +0200 wenzelm tuned;
Tue, 21 Sep 1999 17:28:33 +0200 wenzelm added some ~= rules;
Tue, 21 Sep 1999 17:28:02 +0200 wenzelm removed "case" thm;
Tue, 21 Sep 1999 17:26:50 +0200 wenzelm setup for refined facts handling;
Tue, 21 Sep 1999 17:26:42 +0200 wenzelm setup for refined facts handling;
Tue, 21 Sep 1999 17:24:50 +0200 wenzelm export prems_of;
Tue, 21 Sep 1999 17:24:35 +0200 wenzelm setup_goal: do not insert assumptions;
Tue, 21 Sep 1999 17:23:55 +0200 wenzelm setup for refined facts handling;
Tue, 21 Sep 1999 17:07:28 +0200 wenzelm differ: compare actual props only (hyps may changed due to trivial steps involving assumptions);
Tue, 21 Sep 1999 17:06:49 +0200 wenzelm added bang_facts;
Tue, 21 Sep 1999 14:21:53 +0200 nipkow Added comments.
Tue, 21 Sep 1999 14:16:08 +0200 nipkow Now distinguishes discrete from non-distrete types.
Tue, 21 Sep 1999 14:14:14 +0200 nipkow moved inf_of(?) to hologic.
Tue, 21 Sep 1999 14:13:55 +0200 nipkow Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
Tue, 21 Sep 1999 14:13:45 +0200 nipkow ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
Tue, 21 Sep 1999 11:11:09 +0200 paulson new proof of drop_prog_correct for new definition of project_act
Tue, 21 Sep 1999 11:09:24 +0200 paulson project_act no longer has a special case to allow identity actions
Tue, 21 Sep 1999 10:39:33 +0200 paulson fixed SOUNDNESS BUG concerning the map from terms like ?f x y to SVC variables
(0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip