| Sun, 07 Mar 2010 16:39:31 -0800 |
huffman |
generate separate qualified theorem name for each type's reach and take_lemma
|
file |
diff |
annotate
|
| Thu, 23 Jul 2009 23:13:37 +0200 |
wenzelm |
removed obsolete ML proof tools;
|
file |
diff |
annotate
|
| Thu, 23 Jul 2009 18:44:09 +0200 |
wenzelm |
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
|
file |
diff |
annotate
|
| Fri, 20 Mar 2009 17:12:37 +0100 |
wenzelm |
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
|
file |
diff |
annotate
|
| Wed, 03 Dec 2008 15:58:44 +0100 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Fri, 02 Jun 2006 19:41:37 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 01 Jun 2006 23:53:29 +0200 |
huffman |
removed legacy ML scripts
|
file |
diff |
annotate
|
| Mon, 26 Sep 2005 08:41:24 +0200 |
haftmann |
adjusted web link
|
file |
diff |
annotate
|
| Tue, 06 Sep 2005 21:51:17 +0200 |
wenzelm |
converted to Isar theory format;
|
file |
diff |
annotate
|
| Mon, 12 Jul 2004 15:05:30 +0200 |
oheimb |
corrected bibtex entry
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Sat, 01 Dec 2001 18:52:32 +0100 |
wenzelm |
renamed class "term" to "type" (actually "HOL.type");
|
file |
diff |
annotate
|
| Thu, 31 May 2001 20:52:51 +0200 |
wenzelm |
tuned
|
file |
diff |
annotate
|
| Thu, 31 May 2001 16:53:00 +0200 |
oheimb |
added FOCUS including the One-Element Buffer by Manfred Broy
|
file |
diff |
annotate
|