| Wed, 28 Mar 2012 12:28:24 +0200 | huffman | removed references to obsolete theorems | file | diff | annotate |
| Mon, 08 Aug 2011 07:35:42 +0200 | nipkow | removed old recdef and types usage | file | diff | annotate |
| Mon, 08 Nov 2010 00:00:47 +0100 | wenzelm | updated generated files; | file | diff | annotate |
| Fri, 27 Aug 2010 12:40:20 +0200 | wenzelm | proper context for various Thy_Output options, via official configuration options in ML and Isar; | file | diff | annotate |
| Mon, 31 May 2010 21:06:57 +0200 | wenzelm | modernized some structure names, keeping a few legacy aliases; | file | diff | annotate |
| Sat, 08 May 2010 19:14:13 +0200 | wenzelm | unified/simplified Pretty.margin_default; | file | diff | annotate |
| Thu, 11 Feb 2010 08:44:19 +0100 | nipkow | inductive vs inductive_set explanation | file | diff | annotate |
| Thu, 19 Nov 2009 08:19:57 +0100 | nipkow | anti_sym -> antisym | file | diff | annotate |
| Thu, 01 Oct 2009 20:20:45 +0200 | wenzelm | updated generated files; | file | diff | annotate |
| Wed, 17 Jun 2009 10:07:25 +0200 | haftmann | reworked section on type classes | file | diff | annotate |
| Wed, 04 Mar 2009 11:05:29 +0100 | blanchet | Merge. | file | diff | annotate |
| Wed, 04 Mar 2009 10:45:52 +0100 | blanchet | Merge. | file | diff | annotate |
| Tue, 03 Mar 2009 17:05:18 +0100 | nipkow | removed and renamed redundant lemmas | file | diff | annotate |
| Mon, 02 Mar 2009 17:26:23 +0100 | nipkow | name fix | file | diff | annotate |
| Thu, 01 Jan 2009 21:30:13 +0100 | wenzelm | updated generated files; | file | diff | annotate |
| Tue, 18 Nov 2008 18:25:10 +0100 | wenzelm | moved table of standard Isabelle symbols to isar-ref manual; | file | diff | annotate |
| Sun, 20 Jul 2008 11:19:08 +0200 | haftmann | (adjusted) | file | diff | annotate |
| Fri, 27 Jun 2008 09:55:02 +0200 | haftmann | adjusted import | file | diff | annotate |
| Tue, 16 Oct 2007 17:07:40 +0200 | wenzelm | updated; | file | diff | annotate |
| Tue, 26 Jun 2007 15:48:09 +0200 | paulson | changes for type class ring_no_zero_divisors | file | diff | annotate |
| Mon, 25 Jun 2007 16:56:41 +0200 | nipkow | removed theorem | file | diff | annotate |
| Thu, 12 Apr 2007 15:35:29 +0200 | wenzelm | updated; | file | diff | annotate |
| Thu, 09 Nov 2006 11:58:45 +0100 | wenzelm | updated; | file | diff | annotate |
| Tue, 16 May 2006 20:28:02 +0200 | wenzelm | updated; | file | diff | annotate |
| Sat, 18 Mar 2006 18:33:49 +0100 | wenzelm | updated; | file | diff | annotate |
| Mon, 29 Aug 2005 16:25:24 +0200 | wenzelm | updated; | file | diff | annotate |
| Mon, 29 Aug 2005 11:44:23 +0200 | wenzelm | updated; | file | diff | annotate |
| Sun, 28 Aug 2005 19:42:19 +0200 | wenzelm | updated; | file | diff | annotate |
| Tue, 16 Aug 2005 13:42:23 +0200 | wenzelm | updated; | file | diff | annotate |
| Tue, 28 Jun 2005 15:26:32 +0200 | paulson | replacing zabs_def by abs_if | file | diff | annotate |
| Wed, 22 Jun 2005 09:26:18 +0200 | nipkow | *** empty log message *** | file | diff | annotate |
| Thu, 09 Jun 2005 12:06:38 +0200 | wenzelm | updated; | file | diff | annotate |
| Tue, 19 Apr 2005 13:35:01 +0200 | paulson | auto update | file | diff | annotate |
| Fri, 18 Mar 2005 14:31:50 +0100 | paulson | auto update | file | diff | annotate |
| Tue, 01 Feb 2005 18:01:57 +0100 | paulson | the new subst tactic, by Lucas Dixon | file | diff | annotate |
| Thu, 02 Dec 2004 14:47:07 +0100 | nipkow | *** empty log message *** | file | diff | annotate |
| Thu, 19 Feb 2004 17:57:54 +0100 | paulson | new numerics section using type classes | file | diff | annotate |
| Sun, 15 Feb 2004 10:46:37 +0100 | paulson | Polymorphic treatment of binary arithmetic using axclasses | file | diff | annotate |
| Mon, 12 Jan 2004 16:51:45 +0100 | paulson | Added lemmas to Ring_and_Field with slightly modified simplification rules | file | diff | annotate |
| Mon, 15 Dec 2003 16:38:25 +0100 | paulson | more general lemmas for Ring_and_Field | file | diff | annotate |
| Wed, 10 Dec 2003 15:59:34 +0100 | paulson | Moving some theorems from Real/RealArith0.ML | file | diff | annotate |
| Tue, 02 Dec 2003 11:48:15 +0100 | paulson | More re-organising of numerical theorems | file | diff | annotate |
| Tue, 17 Dec 2002 11:05:41 +0100 | paulson | auto-update | file | diff | annotate |
| Thu, 24 Jan 2002 16:37:49 +0100 | wenzelm | updated; | file | diff | annotate |
| Thu, 29 Nov 2001 21:12:37 +0100 | nipkow | *** empty log message *** | file | diff | annotate |
| Mon, 12 Nov 2001 10:56:38 +0100 | paulson | new-style numerals without leading #, along with generic 0 and 1 | file | diff | annotate |
| Mon, 22 Oct 2001 12:01:35 +0200 | paulson | Numerals now work for the integers: the binary numerals for 0 and 1 rewrite | file | diff | annotate |
| Sun, 21 Oct 2001 19:49:29 +0200 | wenzelm | updated; | file | diff | annotate |
| Mon, 08 Oct 2001 12:28:43 +0200 | wenzelm | *** empty log message *** | file | diff | annotate |
| Wed, 08 Aug 2001 14:50:28 +0200 | paulson | Getting it working again with 1' instead of 1 | file | diff | annotate |
| Wed, 28 Feb 2001 12:37:48 +0100 | paulson | auto-update | file | diff | annotate |
| Wed, 21 Feb 2001 15:21:15 +0100 | paulson | revisions in response to comments by Tobias | file | diff | annotate |
| Sun, 21 Jan 2001 19:50:43 +0100 | wenzelm | updated; | file | diff | annotate |
| Fri, 12 Jan 2001 16:07:20 +0100 | paulson | auto update | file | diff | annotate |
| Fri, 05 Jan 2001 15:16:40 +0100 | nipkow | *** empty log message *** | file | diff | annotate |
| Wed, 03 Jan 2001 21:27:15 +0100 | wenzelm | updated; | file | diff | annotate |
| Mon, 18 Dec 2000 16:45:17 +0100 | nipkow | *** empty log message *** | file | diff | annotate |
| Wed, 13 Dec 2000 17:46:49 +0100 | wenzelm | updated; | file | diff | annotate |
| Tue, 12 Dec 2000 11:57:33 +0100 | paulson | auto-updated | file | diff | annotate |
| Wed, 06 Dec 2000 21:10:40 +0100 | wenzelm | updated; | file | diff | annotate |