| 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 |
| Fri, 24 Jul 1998 13:27:23 +0200 | berghofe | Added theorem ex1_implies_ex. | file | diff | annotate |
| Fri, 17 Jul 1998 10:50:01 +0200 | paulson | tidying | file | diff | annotate |
| Tue, 14 Jul 1998 13:29:39 +0200 | paulson | stac now uses CHANGED_GOAL and correctly fails when it has no useful effect, | file | diff | annotate |
| Thu, 08 Jan 1998 17:47:22 +0100 | oheimb | removed Eps_eq, ex1_Eps_eq, and some unnecessary parentheses | file | diff | annotate |
| Tue, 23 Dec 1997 11:40:18 +0100 | paulson | New rules rev_iffD{1,2} | file | diff | annotate |
| Wed, 26 Nov 1997 17:23:18 +0100 | paulson | Added rule impCE' | file | diff | annotate |
| Tue, 04 Nov 1997 20:46:56 +0100 | oheimb | added theorems for Eps | file | diff | annotate |
| Mon, 03 Nov 1997 12:11:34 +0100 | wenzelm | use "hologic.ML"; use "cladata.ML"; use "simpdata.ML"; moved to ROOT.ML; | file | diff | annotate |
| Tue, 28 Oct 1997 17:41:40 +0100 | wenzelm | fixed qed; | file | diff | annotate |
| Fri, 10 Oct 1997 19:02:28 +0200 | wenzelm | fixed dots; | file | diff | annotate |