Mon, 10 Jan 2022 14:05:33 +0100 |
nipkow |
added lemma
|
file |
diff |
annotate
|
Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
Sat, 24 Feb 2018 17:21:35 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
Thu, 15 Feb 2018 12:11:00 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
Fri, 29 Jul 2016 09:49:23 +0200 |
Andreas Lochbihler |
add lemmas contributed by Peter Gammie
|
file |
diff |
annotate
|
Mon, 25 Apr 2016 16:09:26 +0200 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
Sun, 13 Sep 2015 20:20:16 +0200 |
wenzelm |
renamed method "goals" to "goal_cases" to emphasize its meaning;
|
file |
diff |
annotate
|
Fri, 04 Sep 2015 19:22:13 +0200 |
wenzelm |
modernized name space management -- more uniform qualification;
|
file |
diff |
annotate
|
Thu, 25 Jun 2015 23:33:47 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Wed, 17 Jun 2015 11:03:05 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
Sun, 02 Nov 2014 17:20:45 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
Fri, 14 Feb 2014 07:53:46 +0100 |
blanchet |
merged 'Option.map' and 'Option.map_option'
|
file |
diff |
annotate
|
Thu, 24 Oct 2013 10:03:20 +0200 |
traytel |
refactored rtrancl_while; prove termination for finite rtrancl
|
file |
diff |
annotate
|
Thu, 03 Oct 2013 12:34:32 +0200 |
nipkow |
added and generalised lemmas
|
file |
diff |
annotate
|
Wed, 02 Oct 2013 22:32:50 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
Tue, 03 Sep 2013 22:04:23 +0200 |
wenzelm |
tuned proofs -- less guessing;
|
file |
diff |
annotate
|
Wed, 28 Aug 2013 17:11:28 +0200 |
nipkow |
tuned
|
file |
diff |
annotate
|
Wed, 28 Aug 2013 08:56:57 +0200 |
nipkow |
added rtrancl_while
|
file |
diff |
annotate
|
Mon, 17 Dec 2012 15:17:32 +0100 |
traytel |
useful commutative diagram for while_option
|
file |
diff |
annotate
|
Fri, 23 Nov 2012 23:07:38 +0100 |
nipkow |
moved lemma
|
file |
diff |
annotate
|
Sun, 04 Nov 2012 18:41:27 +0100 |
nipkow |
code for while directly, not via while_option
|
file |
diff |
annotate
|
Mon, 30 Jan 2012 17:15:59 +0100 |
blanchet |
rename lambda translation schemes
|
file |
diff |
annotate
|
Tue, 13 Dec 2011 16:53:28 +0100 |
nipkow |
connect while_option with lfp
|
file |
diff |
annotate
|
Mon, 14 Feb 2011 18:28:36 +0100 |
nipkow |
generalized termination lemmas
|
file |
diff |
annotate
|
Tue, 08 Feb 2011 07:42:08 +0100 |
nipkow |
added termination lemmas
|
file |
diff |
annotate
|
Fri, 09 Jul 2010 17:15:03 +0200 |
krauss |
moved example to its own file in HOL/ex
|
file |
diff |
annotate
|
Fri, 09 Jul 2010 16:32:25 +0200 |
krauss |
added "while_option", which needs no well-foundedness; defined "while" in terms of "while_option"
|
file |
diff |
annotate
|
Fri, 27 Mar 2009 10:05:11 +0100 |
haftmann |
normalized imports
|
file |
diff |
annotate
|
Mon, 07 Jul 2008 08:47:17 +0200 |
haftmann |
absolute imports of HOL/*.thy theories
|
file |
diff |
annotate
|
Thu, 26 Jun 2008 10:07:01 +0200 |
haftmann |
established Plain theory and image
|
file |
diff |
annotate
|
Mon, 16 Jul 2007 21:39:56 +0200 |
krauss |
use function package
|
file |
diff |
annotate
|
Thu, 26 Apr 2007 13:33:09 +0200 |
haftmann |
slightly tuned
|
file |
diff |
annotate
|
Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
Sun, 01 Oct 2006 18:29:23 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Mon, 05 Jun 2006 14:22:58 +0200 |
krauss |
Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure".
|
file |
diff |
annotate
|
Sat, 27 May 2006 17:42:02 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Thu, 08 Dec 2005 20:15:50 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Fri, 10 Sep 2004 20:04:14 +0200 |
nipkow |
Added antisymmetry simproc
|
file |
diff |
annotate
|
Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
Thu, 06 May 2004 14:14:18 +0200 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
Fri, 16 Apr 2004 13:51:04 +0200 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
Thu, 18 Dec 2003 08:20:36 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
Thu, 17 Jan 2002 15:06:36 +0100 |
kleing |
registered directly executable version with the code generator
|
file |
diff |
annotate
|
Tue, 23 Oct 2001 22:58:15 +0200 |
wenzelm |
eliminated old numerals;
|
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
|
Fri, 28 Sep 2001 19:17:01 +0200 |
wenzelm |
recdef (permissive);
|
file |
diff |
annotate
|
Tue, 04 Sep 2001 21:10:57 +0200 |
wenzelm |
renamed "antecedent" case to "rule_context";
|
file |
diff |
annotate
|
Fri, 04 May 2001 15:38:48 +0200 |
nipkow |
made same_fst recdef_simp
|
file |
diff |
annotate
|
Sat, 03 Feb 2001 17:43:05 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Mon, 29 Jan 2001 23:54:56 +0100 |
wenzelm |
avoid dead code;
|
file |
diff |
annotate
|
Fri, 26 Jan 2001 15:50:52 +0100 |
nipkow |
Merged Example into While_Combi
|
file |
diff |
annotate
|
Wed, 03 Jan 2001 21:24:29 +0100 |
wenzelm |
recdef_tc;
|
file |
diff |
annotate
|
Thu, 14 Dec 2000 19:37:27 +0100 |
wenzelm |
unsymbolize;
|
file |
diff |
annotate
|
Wed, 13 Dec 2000 09:32:55 +0100 |
nipkow |
small mods.
|
file |
diff |
annotate
|
Thu, 19 Oct 2000 01:48:26 +0200 |
wenzelm |
use RecdefPackage.tcs_of;
|
file |
diff |
annotate
|
Wed, 18 Oct 2000 23:29:49 +0200 |
wenzelm |
A general ``while'' combinator (from main HOL);
|
file |
diff |
annotate
|