| Mon, 20 Jun 2005 22:13:59 +0200 |
wenzelm |
get_thm(s): Name;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 18:35:27 +0200 |
wenzelm |
accomodate change of TheoryDataFun;
|
file |
diff |
annotate
|
| Sat, 11 Jun 2005 22:15:47 +0200 |
wenzelm |
renamed Sign.intern_tycon to Sign.intern_type;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2005 12:03:36 +0200 |
wenzelm |
can (Thm.get_axiom_i thy) name;
|
file |
diff |
annotate
|
| Sun, 05 Jun 2005 23:07:25 +0200 |
wenzelm |
Type.freeze;
|
file |
diff |
annotate
|
| Thu, 02 Jun 2005 18:29:55 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 31 May 2005 11:53:40 +0200 |
wenzelm |
Theory.restore_naming;
|
file |
diff |
annotate
|
| Thu, 21 Apr 2005 22:02:06 +0200 |
wenzelm |
superceded by Pure.thy and CPure.thy;
|
file |
diff |
annotate
|
| Thu, 21 Apr 2005 19:13:03 +0200 |
berghofe |
Adapted to new interface of instantiation and unification / matching functions.
|
file |
diff |
annotate
|
| Fri, 04 Mar 2005 15:07:34 +0100 |
skalberg |
Removed practically all references to Library.foldr.
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Mon, 24 Jan 2005 17:59:48 +0100 |
berghofe |
Adapted to modified interface of PureThy.get_thm(s).
|
file |
diff |
annotate
|
| Fri, 10 Dec 2004 16:57:01 +0100 |
berghofe |
Added term cache to function condrew in order to speed up rewriting.
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Tue, 01 Jun 2004 12:33:50 +0200 |
wenzelm |
removed obsolete sort 'logic';
|
file |
diff |
annotate
|
| Fri, 19 Mar 2004 10:42:38 +0100 |
paulson |
Removing the datatype declaration of "order" allows the standard General.order
|
file |
diff |
annotate
|
| Wed, 29 Jan 2003 17:32:01 +0100 |
berghofe |
Fixed bug in function corr.
|
file |
diff |
annotate
|
| Wed, 27 Nov 2002 17:23:19 +0100 |
berghofe |
Correctness proofs are now modular, too.
|
file |
diff |
annotate
|
| Sun, 17 Nov 2002 23:43:53 +0100 |
berghofe |
Fixed small bug that caused some definitions to be "forgotten".
|
file |
diff |
annotate
|
| Wed, 13 Nov 2002 15:36:06 +0100 |
berghofe |
- exported functions etype_of and mk_typ
|
file |
diff |
annotate
|
| Mon, 30 Sep 2002 16:42:46 +0200 |
berghofe |
Added check for axioms with "realizes Null A = A".
|
file |
diff |
annotate
|
| Wed, 24 Jul 2002 16:16:44 +0200 |
berghofe |
Tuned type constraint of function merge_rules to make smlnj happy.
|
file |
diff |
annotate
|
| Sun, 21 Jul 2002 15:37:04 +0200 |
berghofe |
Added program extraction module.
|
file |
diff |
annotate
|