| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 22:02:00 +1100 |
kleing |
tuned definition
|
file |
diff |
annotate
|
| Thu, 14 Nov 2013 10:59:22 +0100 |
nipkow |
tuned to improve automation (for REPEAT)
|
file |
diff |
annotate
|
| Fri, 27 Sep 2013 17:57:30 +0200 |
nipkow |
hide coercion
|
file |
diff |
annotate
|
| Wed, 25 Sep 2013 15:49:09 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Wed, 25 Sep 2013 11:56:33 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 16:25:47 +0200 |
wenzelm |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
file |
diff |
annotate
|
| Sat, 10 Aug 2013 10:15:30 +0200 |
kleing |
avoid unnecessary case distinction
|
file |
diff |
annotate
|
| Fri, 09 Aug 2013 12:27:29 +0200 |
kleing |
removed commented out declaration
|
file |
diff |
annotate
|
| Thu, 08 Aug 2013 18:13:12 +0200 |
kleing |
avoid re-inventing transitive closure
|
file |
diff |
annotate
|
| Thu, 08 Aug 2013 14:47:24 +0200 |
kleing |
snippet for instr type
|
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
|
| Sun, 24 Feb 2013 13:46:14 +1100 |
kleing |
eliminated isize in favour of size + type coercion
|
file |
diff |
annotate
|
| Tue, 20 Nov 2012 17:49:26 +0100 |
nipkow |
tuned proof
|
file |
diff |
annotate
|
| Wed, 14 Nov 2012 14:45:14 +0100 |
nipkow |
tuned text
|
file |
diff |
annotate
|
| Wed, 14 Nov 2012 14:11:47 +0100 |
nipkow |
replaced relation by function - simplifies development
|
file |
diff |
annotate
|
| Sat, 28 Apr 2012 07:38:22 +0200 |
nipkow |
renamed Semi to Seq
|
file |
diff |
annotate
|
| Fri, 25 Nov 2011 12:18:33 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Wed, 23 Nov 2011 07:44:56 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Thu, 03 Nov 2011 18:10:13 +1100 |
kleing |
string -> vname
|
file |
diff |
annotate
|
| Thu, 03 Nov 2011 16:22:29 +1100 |
kleing |
JMPF(LESS|GE) -> JMP(LESS|GE) because jumps are int now.
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 16:32:12 +0200 |
nipkow |
renamed B to Bc
|
file |
diff |
annotate
|
| Wed, 12 Oct 2011 20:16:48 +0200 |
wenzelm |
tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
|
file |
diff |
annotate
|
| Thu, 29 Sep 2011 21:42:03 +0200 |
Jean Pichon |
fixed typos in IMP
|
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
|
| Thu, 04 Aug 2011 16:49:57 +0200 |
kleing |
new state syntax with less conflicts
|
file |
diff |
annotate
|
| Thu, 28 Jul 2011 16:56:14 +0200 |
kleing |
compiler proof cleanup
|
file |
diff |
annotate
|
| Thu, 28 Jul 2011 15:15:26 +0200 |
kleing |
resolved code_pred FIXME in IMP; clearer notation for exec_n
|
file |
diff |
annotate
|
| Fri, 17 Jun 2011 20:38:43 +0200 |
kleing |
IMP compiler with int, added reverse soundness direction
|
file |
diff |
annotate
|