| Wed, 26 Dec 2018 16:25:20 +0100 |
wenzelm |
isabelle update_cartouches -t;
|
file |
diff |
annotate
|
| Mon, 20 Aug 2018 20:54:26 +0200 |
nipkow |
avoid session qualification because no tex is generated when used;
|
file |
diff |
annotate
|
| Fri, 12 Jan 2018 14:08:53 +0100 |
wenzelm |
isabelle update_cartouches -c;
|
file |
diff |
annotate
|
| Mon, 09 Jan 2017 19:32:40 +0100 |
nipkow |
hide global sum
|
file |
diff |
annotate
|
| Thu, 27 Aug 2015 19:55:43 +0200 |
blanchet |
fixed typo in comment
|
file |
diff |
annotate
|
| Sun, 21 Sep 2014 16:56:11 +0200 |
haftmann |
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
|
file |
diff |
annotate
|
| 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
|