| Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
| Tue, 06 Oct 2015 15:14:28 +0200 |
wenzelm |
fewer aliases for toplevel theorem statements;
|
file |
diff |
annotate
|
| Wed, 25 Mar 2015 10:44:57 +0100 |
wenzelm |
prefer local fixes;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:16:19 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 19:32:36 +0200 |
blanchet |
updated news
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 11:07:47 +0100 |
wenzelm |
tuned signature -- rearranged modules;
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 07:07:07 +0100 |
nipkow |
enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
|
file |
diff |
annotate
|
| Sun, 16 Feb 2014 18:39:40 +0100 |
blanchet |
folded 'Option.set' into BNF-generated 'set_option'
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Mon, 27 Feb 2012 17:40:59 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 16:14:22 +0100 |
wenzelm |
tuned white space;
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Mon, 26 Jul 2010 17:41:26 +0200 |
wenzelm |
modernized/unified some specifications;
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 23:35:43 +0200 |
wenzelm |
mark schematic statements explicitly;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 13:40:23 +0100 |
haftmann |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file |
diff |
annotate
|
| Wed, 10 Feb 2010 00:45:16 +0100 |
wenzelm |
modernized syntax translations, using mostly abbreviation/notation;
|
file |
diff |
annotate
|
| Fri, 27 Nov 2009 08:42:50 +0100 |
haftmann |
Inl and Inr now with authentic syntax
|
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
|
| Mon, 31 Aug 2009 14:09:42 +0200 |
nipkow |
tuned the simp rules for Int involving insert and intervals.
|
file |
diff |
annotate
|
| Mon, 18 May 2009 23:15:38 +0200 |
nipkow |
fine-tuned elimination of comprehensions involving x=t.
|
file |
diff |
annotate
|
| Sat, 16 May 2009 11:28:02 +0200 |
nipkow |
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:47:20 +0100 |
nipkow |
Made Option a separate theory and renamed option_map to Option.map
|
file |
diff |
annotate
|
| Tue, 07 Oct 2008 16:07:50 +0200 |
haftmann |
arbitrary is undefined
|
file |
diff |
annotate
|
| Sat, 29 Mar 2008 19:14:00 +0100 |
wenzelm |
replaced 'ML_setup' by 'ML';
|
file |
diff |
annotate
|
| Wed, 19 Mar 2008 22:50:42 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Sat, 28 Jul 2007 20:40:22 +0200 |
wenzelm |
tuned ML/simproc declarations;
|
file |
diff |
annotate
|
| Sun, 15 Apr 2007 23:25:49 +0200 |
wenzelm |
avoid internal names;
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 23:42:39 +0200 |
wenzelm |
replaced syntax/translations by abbreviation;
|
file |
diff |
annotate
|
| Wed, 04 Jan 2006 19:22:53 +0100 |
nipkow |
Reversed Larry's option/iff change.
|
file |
diff |
annotate
|
| Tue, 03 Jan 2006 11:32:55 +0100 |
haftmann |
class now an keyword, quoted where necessary
|
file |
diff |
annotate
|
| Wed, 21 Dec 2005 12:02:57 +0100 |
paulson |
removed or modified some instances of [iff]
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Wed, 14 May 2003 20:29:18 +0200 |
schirmer |
Adapted to changes in Map.thy
|
file |
diff |
annotate
|
| Thu, 31 Oct 2002 18:27:10 +0100 |
schirmer |
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
|
file |
diff |
annotate
|
| Tue, 27 Aug 2002 11:03:05 +0200 |
wenzelm |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 22 Feb 2002 11:26:44 +0100 |
schirmer |
Added check for field/method access to operational semantics and proved the acesses valid.
|
file |
diff |
annotate
|
| Mon, 28 Jan 2002 18:51:48 +0100 |
wenzelm |
GPLed;
|
file |
diff |
annotate
|
| Mon, 28 Jan 2002 18:50:23 +0100 |
wenzelm |
tuned header;
|
file |
diff |
annotate
|
| Mon, 28 Jan 2002 17:00:19 +0100 |
schirmer |
Isabelle/Bali sources;
|
file |
diff |
annotate
|