| Thu, 09 Oct 2003 18:13:32 +0200 |
skalberg |
Added support for making constants final, that is, ensuring that no
|
file |
diff |
annotate
|
| Thu, 10 Oct 2002 14:21:49 +0200 |
berghofe |
Added choice_eq.
|
file |
diff |
annotate
|
| Fri, 01 Mar 2002 22:28:59 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 28 Oct 2001 21:14:56 +0100 |
wenzelm |
tuned declaration of rules;
|
file |
diff |
annotate
|
| Sun, 14 Oct 2001 20:00:32 +0200 |
wenzelm |
added ML bindings from former theory Ord;
|
file |
diff |
annotate
|
| Thu, 27 Sep 2001 16:04:11 +0200 |
wenzelm |
AddXEs [disjI1, disjI2];
|
file |
diff |
annotate
|
| Wed, 25 Jul 2001 13:13:01 +0200 |
paulson |
partial restructuring to reduce dependence on Axiom of Choice
|
file |
diff |
annotate
|
| Fri, 10 Nov 2000 19:03:06 +0100 |
wenzelm |
axclass power moved to Nat.thy;
|
file |
diff |
annotate
|
| Thu, 19 Oct 2000 21:20:53 +0200 |
wenzelm |
declare sym [elim?] in HOL.ML instead of Calculation.thy;
|
file |
diff |
annotate
|
| Tue, 10 Oct 2000 23:43:23 +0200 |
wenzelm |
AddXEs [someI_ex];
|
file |
diff |
annotate
|
| Fri, 22 Sep 2000 17:24:36 +0200 |
wenzelm |
AddXIs [equal_intr_rule];
|
file |
diff |
annotate
|
| Sun, 17 Sep 2000 22:24:52 +0200 |
wenzelm |
AddXIs [ext];
|
file |
diff |
annotate
|
| Fri, 15 Sep 2000 15:30:50 +0200 |
paulson |
the final renaming: selectI -> someI
|
file |
diff |
annotate
|
| Fri, 21 Jul 2000 12:30:08 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Thu, 09 Sep 1999 12:25:30 +0200 |
wenzelm |
AddXIs [disjI1, disjI2];
|
file |
diff |
annotate
|
| Wed, 25 Aug 1999 20:49:02 +0200 |
wenzelm |
proper bootstrap of HOL theory and packages;
|
file |
diff |
annotate
|
| Mon, 19 Jul 1999 15:19:11 +0200 |
paulson |
getting rid of qed_goal
|
file |
diff |
annotate
|
| Sat, 10 Jul 1999 21:48:27 +0200 |
wenzelm |
handle THM/TERM exn;
|
file |
diff |
annotate
|
| Tue, 27 Apr 1999 10:43:52 +0200 |
wenzelm |
hol_setup;
|
file |
diff |
annotate
|
| Thu, 15 Apr 1999 18:10:37 +0200 |
nipkow |
Added new thms.
|
file |
diff |
annotate
|
| Wed, 03 Feb 1999 17:33:20 +0100 |
wenzelm |
ThmDatabase.ml_store_thm;
|
file |
diff |
annotate
|
| Tue, 12 Jan 1999 13:54:51 +0100 |
wenzelm |
eliminated tthm type and Attribute structure;
|
file |
diff |
annotate
|
| Mon, 16 Nov 1998 11:11:58 +0100 |
wenzelm |
attrib_setup: rulify;
|
file |
diff |
annotate
|
| Mon, 09 Nov 1998 10:58:49 +0100 |
paulson |
removed obsolete comment and "open" declaration
|
file |
diff |
annotate
|
| Fri, 23 Oct 1998 22:36:15 +0200 |
berghofe |
Added theorems True_not_False and False_not_True
|
file |
diff |
annotate
|
| Wed, 09 Sep 1998 17:34:58 +0200 |
nipkow |
Proved and added rewrite rule (@x. x=y) = y to simpset.
|
file |
diff |
annotate
|
| Thu, 20 Aug 1998 09:25:59 +0200 |
paulson |
Now qed_spec_mp respects locales, by calling ml_store_thm
|
file |
diff |
annotate
|
| Thu, 13 Aug 1998 17:28:52 +0200 |
paulson |
stac now handles definitions as well as equalities
|
file |
diff |
annotate
|
| Wed, 12 Aug 1998 15:40:47 +0200 |
oheimb |
added Eps_eq
|
file |
diff |
annotate
|
| Fri, 31 Jul 1998 11:03:31 +0200 |
wenzelm |
isatool expandshort;
|
file |
diff |
annotate
|