| 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 |