| Wed, 23 Sep 2020 15:18:07 +0200 |
\----- start update Isabelle2019 --> Isabelle2020
|
file | diff | annotate |
| Tue, 03 Sep 2019 16:10:31 +0200 |
\----- start update Isabelle2018 --> Isabelle2019
|
file | diff | annotate |
| Wed, 22 Aug 2018 14:44:15 +0200 |
\----- start update Isabelle2017 --> Isabelle2018
|
file | diff | annotate |
| Fri, 19 Jan 2018 12:49:17 +0100 |
\----- start update Isabelle2015 --> Isabelle2017
|
file | diff | annotate |
| Sat, 05 Dec 2015 16:09:41 +0100 |
switched from Isabelle2014 to Isabelle2015, intermediate state
|
file | diff | annotate |
| Wed, 19 Feb 2014 22:02:00 +1100 |
tuned definition
|
file | diff | annotate |
| Thu, 14 Nov 2013 10:59:22 +0100 |
tuned to improve automation (for REPEAT)
|
file | diff | annotate |
| Fri, 27 Sep 2013 17:57:30 +0200 |
hide coercion
|
file | diff | annotate |
| Wed, 25 Sep 2013 15:49:09 +0200 |
tuned
|
file | diff | annotate |
| Wed, 25 Sep 2013 11:56:33 +0200 |
tuned
|
file | diff | annotate |
| Tue, 13 Aug 2013 16:25:47 +0200 |
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 |
avoid unnecessary case distinction
|
file | diff | annotate |
| Fri, 09 Aug 2013 12:27:29 +0200 |
removed commented out declaration
|
file | diff | annotate |
| Thu, 08 Aug 2013 18:13:12 +0200 |
avoid re-inventing transitive closure
|
file | diff | annotate |
| Thu, 08 Aug 2013 14:47:24 +0200 |
snippet for instr type
|
file | diff | annotate |
| Fri, 17 May 2013 08:19:52 +0200 |
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
|
file | diff | annotate |
| Sun, 24 Feb 2013 13:46:14 +1100 |
eliminated isize in favour of size + type coercion
|
file | diff | annotate |
| Tue, 20 Nov 2012 17:49:26 +0100 |
tuned proof
|
file | diff | annotate |
| Wed, 14 Nov 2012 14:45:14 +0100 |
tuned text
|
file | diff | annotate |
| Wed, 14 Nov 2012 14:11:47 +0100 |
replaced relation by function - simplifies development
|
file | diff | annotate |
| Sat, 28 Apr 2012 07:38:22 +0200 |
renamed Semi to Seq
|
file | diff | annotate |
| Fri, 25 Nov 2011 12:18:33 +0100 |
tuned
|
file | diff | annotate |
| Wed, 23 Nov 2011 07:44:56 +0100 |
tuned
|
file | diff | annotate |
| Thu, 03 Nov 2011 18:10:13 +1100 |
string -> vname
|
file | diff | annotate |
| Thu, 03 Nov 2011 16:22:29 +1100 |
JMPF(LESS|GE) -> JMP(LESS|GE) because jumps are int now.
|
file | diff | annotate |
| Wed, 19 Oct 2011 16:32:12 +0200 |
renamed B to Bc
|
file | diff | annotate |
| Wed, 12 Oct 2011 20:16:48 +0200 |
tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
|
file | diff | annotate |
| Thu, 29 Sep 2011 21:42:03 +0200 |
fixed typos in IMP
|
file | diff | annotate |
| Tue, 20 Sep 2011 05:48:23 +0200 |
Updated IMP to use new induction method
|
file | diff | annotate |
| Mon, 12 Sep 2011 07:55:43 +0200 |
new fastforce replacing fastsimp - less confusing name
|
file | diff | annotate |
| Thu, 04 Aug 2011 16:49:57 +0200 |
new state syntax with less conflicts
|
file | diff | annotate |
| Thu, 28 Jul 2011 16:56:14 +0200 |
compiler proof cleanup
|
file | diff | annotate |
| Thu, 28 Jul 2011 15:15:26 +0200 |
resolved code_pred FIXME in IMP; clearer notation for exec_n
|
file | diff | annotate |
| Fri, 17 Jun 2011 20:38:43 +0200 |
IMP compiler with int, added reverse soundness direction
|
file | diff | annotate |
| Mon, 06 Jun 2011 16:29:38 +0200 |
imported rest of new IMP
|
file | diff | annotate |
| Wed, 01 Jun 2011 21:35:34 +0200 |
Replacing old IMP with new Semantics material
|
file | diff | annotate |
| Sat, 17 Oct 2009 14:43:18 +0200 |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file | diff | annotate |
| Thu, 09 Jul 2009 17:33:22 +0200 |
drop unused lemmas
|
file | diff | annotate |
| Wed, 25 Jun 2008 22:01:34 +0200 |
modernized specifications;
|
file | diff | annotate |
| Wed, 11 Jul 2007 11:14:51 +0200 |
Adapted to new inductive definition package.
|
file | diff | annotate |
| Wed, 26 Jul 2006 19:23:04 +0200 |
linear arithmetic splits certain operators (e.g. min, max, abs)
|
file | diff | annotate |
| Fri, 17 Jun 2005 16:12:49 +0200 |
migrated theory headers to new format
|
file | diff | annotate |
| Tue, 11 May 2004 20:11:08 +0200 |
changes made due to new Ring_and_Field theory
|
file | diff | annotate |
| Thu, 24 Oct 2002 07:23:46 +0200 |
ASIN -> SET
|
file | diff | annotate |
| Tue, 08 Oct 2002 08:20:17 +0200 |
Got rid of rotates because of new simplifier
|
file | diff | annotate |
| Fri, 26 Apr 2002 11:47:01 +0200 |
New machine architecture and other direction of compiler proof.
|
file | diff | annotate |
| Thu, 20 Dec 2001 18:22:44 +0100 |
renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
|
file | diff | annotate |
| Wed, 19 Dec 2001 00:26:04 +0100 |
tuned;
|
file | diff | annotate |
| Sun, 09 Dec 2001 14:34:56 +0100 |
tuned for latex output
|
file | diff | annotate |
| Fri, 23 Nov 2001 17:19:14 +0100 |
Isar conversion
|
file | diff | annotate |
| Sat, 06 Oct 2001 00:02:46 +0200 |
* sane numerals (stage 2): plain "num" syntax (removed "#");
|
file | diff | annotate |
| Fri, 05 Oct 2001 21:52:39 +0200 |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
|
file | diff | annotate |
| Mon, 30 Apr 2001 19:26:04 +0200 |
new proof
|
file | diff | annotate |
| Fri, 10 Nov 2000 09:17:54 +0100 |
JMB -> JMPB. Email von Johannes Pfeifroth.
|
file | diff | annotate |
| Thu, 26 Oct 2000 14:59:38 +0200 |
*** empty log message ***
|
file | diff | annotate |
| Thu, 26 Oct 2000 14:52:41 +0200 |
*** empty log message ***
|
file | diff | annotate |