| Mon, 30 Jan 2012 17:15:59 +0100 |
blanchet |
rename lambda translation schemes
|
file |
diff |
annotate
|
| Tue, 13 Dec 2011 16:53:28 +0100 |
nipkow |
connect while_option with lfp
|
file |
diff |
annotate
|
| Mon, 14 Feb 2011 18:28:36 +0100 |
nipkow |
generalized termination lemmas
|
file |
diff |
annotate
|
| Tue, 08 Feb 2011 07:42:08 +0100 |
nipkow |
added termination lemmas
|
file |
diff |
annotate
|
| Fri, 09 Jul 2010 17:15:03 +0200 |
krauss |
moved example to its own file in HOL/ex
|
file |
diff |
annotate
|
| Fri, 09 Jul 2010 16:32:25 +0200 |
krauss |
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
|
file |
diff |
annotate
|
| Fri, 27 Mar 2009 10:05:11 +0100 |
haftmann |
normalized imports
|
file |
diff |
annotate
|
| Mon, 07 Jul 2008 08:47:17 +0200 |
haftmann |
absolute imports of HOL/*.thy theories
|
file |
diff |
annotate
|
| Thu, 26 Jun 2008 10:07:01 +0200 |
haftmann |
established Plain theory and image
|
file |
diff |
annotate
|
| Mon, 16 Jul 2007 21:39:56 +0200 |
krauss |
use function package
|
file |
diff |
annotate
|
| Thu, 26 Apr 2007 13:33:09 +0200 |
haftmann |
slightly tuned
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Sun, 01 Oct 2006 18:29:23 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 05 Jun 2006 14:22:58 +0200 |
krauss |
Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure".
|
file |
diff |
annotate
|
| Sat, 27 May 2006 17:42:02 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 08 Dec 2005 20:15:50 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 10 Sep 2004 20:04:14 +0200 |
nipkow |
Added antisymmetry simproc
|
file |
diff |
annotate
|
| Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
| Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
| Thu, 06 May 2004 14:14:18 +0200 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
| Fri, 16 Apr 2004 13:51:04 +0200 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
| Thu, 18 Dec 2003 08:20:36 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Thu, 17 Jan 2002 15:06:36 +0100 |
kleing |
registered directly executable version with the code generator
|
file |
diff |
annotate
|
| Tue, 23 Oct 2001 22:58:15 +0200 |
wenzelm |
eliminated old numerals;
|
file |
diff |
annotate
|
| Sat, 06 Oct 2001 00:02:46 +0200 |
wenzelm |
* sane numerals (stage 2): plain "num" syntax (removed "#");
|
file |
diff |
annotate
|
| Fri, 05 Oct 2001 21:52:39 +0200 |
wenzelm |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
|
file |
diff |
annotate
|
| Fri, 28 Sep 2001 19:17:01 +0200 |
wenzelm |
recdef (permissive);
|
file |
diff |
annotate
|
| Tue, 04 Sep 2001 21:10:57 +0200 |
wenzelm |
renamed "antecedent" case to "rule_context";
|
file |
diff |
annotate
|
| Fri, 04 May 2001 15:38:48 +0200 |
nipkow |
made same_fst recdef_simp
|
file |
diff |
annotate
|
| Sat, 03 Feb 2001 17:43:05 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|