| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| Mon, 08 Jul 2013 14:24:36 +0200 |
nipkow |
tuned proofs
|
file |
diff |
annotate
|
| Fri, 05 Jul 2013 16:45:31 +0200 |
nipkow |
improved proof automation for numerals
|
file |
diff |
annotate
|
| Sun, 26 May 2013 11:56:55 +0200 |
nipkow |
simpler proof through custom summation function
|
file |
diff |
annotate
|
| Wed, 22 May 2013 08:46:39 +0200 |
nipkow |
simplified example and proof
|
file |
diff |
annotate
|
| Fri, 17 May 2013 08:19:52 +0200 |
nipkow |
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
|
file |
diff |
annotate
|
| Sat, 19 Jan 2013 21:05:05 +0100 |
nipkow |
simplified proofs
|
file |
diff |
annotate
|
| Sat, 28 Apr 2012 07:38:22 +0200 |
nipkow |
renamed Semi to Seq
|
file |
diff |
annotate
|
| Tue, 20 Sep 2011 05:48:23 +0200 |
nipkow |
Updated IMP to use new induction method
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Sat, 13 Aug 2011 11:57:13 +0200 |
kleing |
IMP/Util distinguishes between sets and functions again; imported only where used.
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 16:29:38 +0200 |
kleing |
imported rest of new IMP
|
file |
diff |
annotate
|