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