| 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
|
| 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
|
| Sun, 10 Aug 1997 12:28:34 +0200 |
nipkow |
Added select1_equality
|
file |
diff |
annotate
|
| Wed, 06 Aug 1997 11:57:20 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Wed, 06 Aug 1997 01:13:46 +0200 |
berghofe |
Moved some functions which used to be part of thy_data.ML
|
file |
diff |
annotate
|
| Fri, 13 Jun 1997 10:35:13 +0200 |
nipkow |
Tuned wf_iff_no_infinite_down_chain proof, based on Konrads ideas.
|
file |
diff |
annotate
|
| Mon, 21 Apr 1997 12:16:04 +0200 |
paulson |
New introduction rule for "unique existence"
|
file |
diff |
annotate
|
| Wed, 29 Jan 1997 15:32:18 +0100 |
paulson |
Moved qed_spec_mp, etc., from HOL.ML to thy_data.ML so that they work
|
file |
diff |
annotate
|
| Wed, 18 Dec 1996 15:11:07 +0100 |
oheimb |
added qed_goal_spec_mp and qed_goalw_spec_mp
|
file |
diff |
annotate
|
| Thu, 26 Sep 1996 12:47:47 +0200 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
| Thu, 12 Sep 1996 10:34:01 +0200 |
paulson |
Split off classical reasoning code to cladata.ML
|
file |
diff |
annotate
|
| Mon, 19 Aug 1996 11:33:08 +0200 |
paulson |
Improved comment
|
file |
diff |
annotate
|
| Fri, 28 Jun 1996 15:27:53 +0200 |
paulson |
Added rev_notE by analogy with rev_mp
|
file |
diff |
annotate
|
| Tue, 07 May 1996 09:53:20 +0200 |
berghofe |
Added function for storing default claset in theory.
|
file |
diff |
annotate
|
| Tue, 23 Apr 1996 16:58:21 +0200 |
oheimb |
repaired critical proofs depending on the order inside non-confluent SimpSets,
|
file |
diff |
annotate
|
| Fri, 19 Apr 1996 11:33:24 +0200 |
clasohm |
added Konrad's code for the datatype package
|
file |
diff |
annotate
|
| Wed, 17 Apr 1996 17:59:58 +0200 |
oheimb |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 12 Apr 1996 12:41:26 +0200 |
clasohm |
changed first parameter of add_thydata and get_thydata
|
file |
diff |
annotate
|
| Mon, 19 Feb 1996 18:04:41 +0100 |
nipkow |
Introduced normalize_thm into HOL.ML
|
file |
diff |
annotate
|
| Fri, 09 Feb 1996 13:41:18 +0100 |
nipkow |
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
|
file |
diff |
annotate
|
| Tue, 30 Jan 1996 15:24:36 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Mon, 29 Jan 1996 13:48:37 +0100 |
clasohm |
changed the way simpsets and information about datatypes are stored
|
file |
diff |
annotate
|