| 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
|
| Mon, 06 Jun 2011 16:29:38 +0200 |
kleing |
imported rest of new IMP
|
file |
diff |
annotate
|
| Wed, 01 Jun 2011 21:35:34 +0200 |
nipkow |
Replacing old IMP with new Semantics material
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Thu, 09 Jul 2009 17:33:22 +0200 |
krauss |
drop unused lemmas
|
file |
diff |
annotate
|
| Wed, 25 Jun 2008 22:01:34 +0200 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:14:51 +0200 |
berghofe |
Adapted to new inductive definition package.
|
file |
diff |
annotate
|
| Wed, 26 Jul 2006 19:23:04 +0200 |
webertj |
linear arithmetic splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Tue, 11 May 2004 20:11:08 +0200 |
obua |
changes made due to new Ring_and_Field theory
|
file |
diff |
annotate
|
| Thu, 24 Oct 2002 07:23:46 +0200 |
nipkow |
ASIN -> SET
|
file |
diff |
annotate
|
| Tue, 08 Oct 2002 08:20:17 +0200 |
nipkow |
Got rid of rotates because of new simplifier
|
file |
diff |
annotate
|
| Fri, 26 Apr 2002 11:47:01 +0200 |
nipkow |
New machine architecture and other direction of compiler proof.
|
file |
diff |
annotate
|
| Thu, 20 Dec 2001 18:22:44 +0100 |
nipkow |
renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
|
file |
diff |
annotate
|
| Wed, 19 Dec 2001 00:26:04 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 09 Dec 2001 14:34:56 +0100 |
kleing |
tuned for latex output
|
file |
diff |
annotate
|
| Fri, 23 Nov 2001 17:19:14 +0100 |
nipkow |
Isar conversion
|
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
|
| Mon, 30 Apr 2001 19:26:04 +0200 |
nipkow |
new proof
|
file |
diff |
annotate
|
| Fri, 10 Nov 2000 09:17:54 +0100 |
nipkow |
JMB -> JMPB. Email von Johannes Pfeifroth.
|
file |
diff |
annotate
|
| Thu, 26 Oct 2000 14:59:38 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Thu, 26 Oct 2000 14:52:41 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|