Thu, 02 Sep 1999 15:22:15 +0200 wenzelm with_path;
Thu, 02 Sep 1999 15:21:36 +0200 wenzelm renamed improper method 'clarsimp' to 'clarsimp_tac';
Wed, 01 Sep 1999 21:46:01 +0200 wenzelm added MultisetOrder.thy;
Wed, 01 Sep 1999 21:45:48 +0200 wenzelm Isar_examples/MultisetOrder.thy;
Wed, 01 Sep 1999 21:35:39 +0200 wenzelm tuned;
Wed, 01 Sep 1999 21:35:20 +0200 wenzelm "this";
Wed, 01 Sep 1999 21:35:04 +0200 wenzelm Wellfoundedness proof for the multiset order (preliminary version).
Wed, 01 Sep 1999 21:28:56 +0200 wenzelm fix: vars;
Wed, 01 Sep 1999 21:28:42 +0200 wenzelm removed "*" method combinator;
Wed, 01 Sep 1999 21:26:26 +0200 wenzelm observe show_types;
Wed, 01 Sep 1999 21:25:55 +0200 wenzelm bind_thms;
Wed, 01 Sep 1999 21:25:17 +0200 wenzelm bind_thm "case";
Wed, 01 Sep 1999 21:24:50 +0200 wenzelm *: no quotes;
Wed, 01 Sep 1999 21:24:23 +0200 wenzelm Method.insert_tac;
Wed, 01 Sep 1999 21:22:56 +0200 wenzelm Method.insert_tac;
Wed, 01 Sep 1999 21:22:38 +0200 wenzelm Method.insert_tac;
Wed, 01 Sep 1999 21:21:22 +0200 wenzelm bind_thm;
Wed, 01 Sep 1999 21:21:01 +0200 wenzelm added bind_thms, store_thms;
Wed, 01 Sep 1999 21:20:04 +0200 wenzelm structures Vartab / Termtab (instances of TableFun);
Wed, 01 Sep 1999 21:19:37 +0200 wenzelm tuned;
Wed, 01 Sep 1999 21:17:37 +0200 wenzelm any_props: improved error;
Wed, 01 Sep 1999 21:17:03 +0200 wenzelm fix: common constraints;
Wed, 01 Sep 1999 21:16:23 +0200 wenzelm Thm.def_name;
Wed, 01 Sep 1999 21:15:52 +0200 wenzelm replaced IsarCmd.kill_theory by Toplevel.kill;
Wed, 01 Sep 1999 21:14:23 +0200 wenzelm calculation: thm list;
Wed, 01 Sep 1999 21:13:12 +0200 wenzelm removed kill_theory;
Wed, 01 Sep 1999 21:11:44 +0200 wenzelm removed the_fact;
Wed, 01 Sep 1999 21:10:05 +0200 wenzelm fix: common constraints;
Wed, 01 Sep 1999 21:09:10 +0200 wenzelm added store/bind_thms;
Wed, 01 Sep 1999 21:06:57 +0200 wenzelm added theorems;
Wed, 01 Sep 1999 21:06:27 +0200 wenzelm added theorems;
Wed, 01 Sep 1999 21:05:48 +0200 wenzelm isar: avoid verbose goal responses;
Wed, 01 Sep 1999 21:05:19 +0200 wenzelm structure Termtab;
Wed, 01 Sep 1999 21:04:59 +0200 wenzelm smart_store_thms;
Wed, 01 Sep 1999 21:04:01 +0200 wenzelm PureThy.smart_store_thms;
Wed, 01 Sep 1999 11:16:02 +0200 paulson tidied some proofs
Wed, 01 Sep 1999 11:15:35 +0200 paulson tidied
Tue, 31 Aug 1999 16:04:43 +0200 paulson tidied
Tue, 31 Aug 1999 15:58:38 +0200 paulson new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
Tue, 31 Aug 1999 15:56:56 +0200 paulson changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
Mon, 30 Aug 1999 23:19:13 +0200 wenzelm proper calculation / induction;
Mon, 30 Aug 1999 20:30:39 +0200 wenzelm tuned;
Mon, 30 Aug 1999 20:30:21 +0200 wenzelm OF: "_" as argument;
Mon, 30 Aug 1999 20:29:28 +0200 wenzelm clean: include HOL-Real-ex;
Mon, 30 Aug 1999 17:26:43 +0200 wenzelm auto: CHANGED;
Mon, 30 Aug 1999 17:18:20 +0200 paulson make it actually RUN the real examples
Mon, 30 Aug 1999 15:25:16 +0200 paulson new directory HOL/Real/ex of real examples
Mon, 30 Aug 1999 14:11:47 +0200 wenzelm 'iff' attribute;
Mon, 30 Aug 1999 14:08:37 +0200 wenzelm 'arith' method;
Mon, 30 Aug 1999 14:08:23 +0200 wenzelm '_' theorem;
Mon, 30 Aug 1999 14:07:48 +0200 wenzelm tuned;
Mon, 30 Aug 1999 11:20:42 +0200 paulson new results for localTo
Mon, 30 Aug 1999 11:20:23 +0200 paulson a new theorem
Mon, 30 Aug 1999 11:13:27 +0200 wenzelm tuned;
Sun, 29 Aug 1999 17:53:03 +0200 wenzelm added MutilatedCheckerboard;
Sun, 29 Aug 1999 17:52:44 +0200 wenzelm added Isar_examples/MutilatedCheckerboard.thy;
Sun, 29 Aug 1999 17:47:26 +0200 wenzelm The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
Fri, 27 Aug 1999 20:29:20 +0200 wenzelm tuned;
Fri, 27 Aug 1999 18:59:27 +0200 wenzelm thm "_" = asm_rl;
Fri, 27 Aug 1999 15:52:32 +0200 paulson tidied
(0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip