Wed, 01 Sep 1999 21:19:37 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Wed, 01 Sep 1999 21:17:37 +0200 |
wenzelm |
any_props: improved error;
|
changeset |
files
|
Wed, 01 Sep 1999 21:17:03 +0200 |
wenzelm |
fix: common constraints;
|
changeset |
files
|
Wed, 01 Sep 1999 21:16:23 +0200 |
wenzelm |
Thm.def_name;
|
changeset |
files
|
Wed, 01 Sep 1999 21:15:52 +0200 |
wenzelm |
replaced IsarCmd.kill_theory by Toplevel.kill;
|
changeset |
files
|
Wed, 01 Sep 1999 21:14:23 +0200 |
wenzelm |
calculation: thm list;
|
changeset |
files
|
Wed, 01 Sep 1999 21:13:12 +0200 |
wenzelm |
removed kill_theory;
|
changeset |
files
|
Wed, 01 Sep 1999 21:11:44 +0200 |
wenzelm |
removed the_fact;
|
changeset |
files
|
Wed, 01 Sep 1999 21:10:05 +0200 |
wenzelm |
fix: common constraints;
|
changeset |
files
|
Wed, 01 Sep 1999 21:09:10 +0200 |
wenzelm |
added store/bind_thms;
|
changeset |
files
|
Wed, 01 Sep 1999 21:06:57 +0200 |
wenzelm |
added theorems;
|
changeset |
files
|
Wed, 01 Sep 1999 21:06:27 +0200 |
wenzelm |
added theorems;
|
changeset |
files
|
Wed, 01 Sep 1999 21:05:48 +0200 |
wenzelm |
isar: avoid verbose goal responses;
|
changeset |
files
|
Wed, 01 Sep 1999 21:05:19 +0200 |
wenzelm |
structure Termtab;
|
changeset |
files
|
Wed, 01 Sep 1999 21:04:59 +0200 |
wenzelm |
smart_store_thms;
|
changeset |
files
|
Wed, 01 Sep 1999 21:04:01 +0200 |
wenzelm |
PureThy.smart_store_thms;
|
changeset |
files
|
Wed, 01 Sep 1999 11:16:02 +0200 |
paulson |
tidied some proofs
|
changeset |
files
|
Wed, 01 Sep 1999 11:15:35 +0200 |
paulson |
tidied
|
changeset |
files
|
Tue, 31 Aug 1999 16:04:43 +0200 |
paulson |
tidied
|
changeset |
files
|
Tue, 31 Aug 1999 15:58:38 +0200 |
paulson |
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
|
changeset |
files
|
Tue, 31 Aug 1999 15:56:56 +0200 |
paulson |
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
|
changeset |
files
|
Mon, 30 Aug 1999 23:19:13 +0200 |
wenzelm |
proper calculation / induction;
|
changeset |
files
|
Mon, 30 Aug 1999 20:30:39 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Mon, 30 Aug 1999 20:30:21 +0200 |
wenzelm |
OF: "_" as argument;
|
changeset |
files
|
Mon, 30 Aug 1999 20:29:28 +0200 |
wenzelm |
clean: include HOL-Real-ex;
|
changeset |
files
|
Mon, 30 Aug 1999 17:26:43 +0200 |
wenzelm |
auto: CHANGED;
|
changeset |
files
|
Mon, 30 Aug 1999 17:18:20 +0200 |
paulson |
make it actually RUN the real examples
|
changeset |
files
|
Mon, 30 Aug 1999 15:25:16 +0200 |
paulson |
new directory HOL/Real/ex of real examples
|
changeset |
files
|
Mon, 30 Aug 1999 14:11:47 +0200 |
wenzelm |
'iff' attribute;
|
changeset |
files
|
Mon, 30 Aug 1999 14:08:37 +0200 |
wenzelm |
'arith' method;
|
changeset |
files
|
Mon, 30 Aug 1999 14:08:23 +0200 |
wenzelm |
'_' theorem;
|
changeset |
files
|
Mon, 30 Aug 1999 14:07:48 +0200 |
wenzelm |
tuned;
|
changeset |
files
|