| Sat, 06 Oct 2007 16:50:04 +0200 | wenzelm | simplified interfaces for outer syntax; | file | diff | annotate |
| Wed, 03 Oct 2007 22:33:17 +0200 | wenzelm | avoid unnamed infixes; | file | diff | annotate |
| Wed, 26 Sep 2007 19:18:00 +0200 | wenzelm | Attrib.eval_thms; | file | diff | annotate |
| Tue, 25 Sep 2007 17:06:14 +0200 | wenzelm | proper Sign operations instead of Theory aliases; | file | diff | annotate |
| Tue, 25 Sep 2007 13:28:37 +0200 | wenzelm | Syntax.parse/check/read; | file | diff | annotate |
| Tue, 14 Aug 2007 13:20:12 +0200 | wenzelm | PrimitiveDefs.mk_defpair; | file | diff | annotate |
| Tue, 19 Jun 2007 23:15:38 +0200 | wenzelm | BalancedTree; | file | diff | annotate |
| Wed, 04 Apr 2007 00:11:03 +0200 | wenzelm | removed obsolete sign_of/sign_of_thm; | file | diff | annotate |
| Fri, 19 Jan 2007 22:08:08 +0100 | wenzelm | moved parts of OuterParse to SpecParse; | file | diff | annotate |
| Tue, 14 Nov 2006 00:15:38 +0100 | wenzelm | incorporated IsarThy into IsarCmd; | file | diff | annotate |
| Sat, 08 Jul 2006 12:54:33 +0200 | wenzelm | Goal.prove_global; | file | diff | annotate |
| Sat, 21 Jan 2006 23:02:14 +0100 | wenzelm | simplified type attribute; | file | diff | annotate |
| Sun, 15 Jan 2006 19:58:53 +0100 | wenzelm | classical attributes: optional weight; | file | diff | annotate |
| Sat, 14 Jan 2006 22:25:34 +0100 | wenzelm | generic attributes; | file | diff | annotate |
| Fri, 16 Dec 2005 09:00:11 +0100 | haftmann | re-arranged tuples (theory * 'a) to ('a * theory) in Pure | file | diff | annotate |
| Fri, 09 Dec 2005 09:06:45 +0100 | haftmann | oriented result pairs in PureThy | file | diff | annotate |
| Tue, 06 Dec 2005 09:04:09 +0100 | haftmann | re-oriented some result tuples in PureThy | file | diff | annotate |
| Wed, 16 Nov 2005 17:45:31 +0100 | wenzelm | Term.betapplys; | file | diff | annotate |
| Tue, 25 Oct 2005 18:18:49 +0200 | wenzelm | avoid legacy goals; | file | diff | annotate |
| Fri, 21 Oct 2005 18:14:38 +0200 | wenzelm | OldGoals; | file | diff | annotate |
| Wed, 19 Oct 2005 21:52:49 +0200 | wenzelm | removed obsolete add_datatype_x; | file | diff | annotate |
| Thu, 15 Sep 2005 17:16:56 +0200 | wenzelm | TableFun/Symtab: curried lookup and update; | file | diff | annotate |
| Mon, 05 Sep 2005 17:38:18 +0200 | wenzelm | curried_lookup/update; | file | diff | annotate |
| Tue, 16 Aug 2005 13:42:26 +0200 | wenzelm | OuterKeyword; | file | diff | annotate |
| Wed, 13 Apr 2005 18:45:25 +0200 | wenzelm | *** MESSAGE REFERS TO PREVIOUS VERSION *** | file | diff | annotate |
| Wed, 13 Apr 2005 18:34:22 +0200 | wenzelm | *** empty log message *** | file | diff | annotate |
| Fri, 04 Mar 2005 15:07:34 +0100 | skalberg | Removed practically all references to Library.foldr. | file | diff | annotate |
| Thu, 03 Mar 2005 12:43:01 +0100 | skalberg | Move towards standard functions. | file | diff | annotate |
| Sun, 13 Feb 2005 17:15:14 +0100 | skalberg | Deleted Library.option type. | file | diff | annotate |
| Mon, 24 Jan 2005 18:12:22 +0100 | berghofe | Replaced xstring by thmref. | file | diff | annotate |
| Wed, 15 May 2002 10:44:58 +0200 | paulson | better error messages for datatypes not declared Const | file | diff | annotate |
| Tue, 12 Feb 2002 20:28:27 +0100 | wenzelm | got rid of explicit marginal comments (now stripped earlier from input); | file | diff | annotate |
| Mon, 19 Nov 2001 20:47:57 +0100 | wenzelm | tuned; | file | diff | annotate |
| Fri, 16 Nov 2001 22:08:55 +0100 | wenzelm | additional P.marg_comment; | file | diff | annotate |
| Wed, 14 Nov 2001 23:18:13 +0100 | wenzelm | use proper intr_names (for required case_names); | file | diff | annotate |
| Wed, 14 Nov 2001 18:46:30 +0100 | wenzelm | adapted primrec/datatype to Isar; | file | diff | annotate |
| Fri, 09 Nov 2001 22:53:10 +0100 | wenzelm | adapted to add_inductive_x; | file | diff | annotate |
| Thu, 13 Jul 2000 23:20:57 +0200 | wenzelm | adapted PureThy.add_defs_i; | file | diff | annotate |
| Fri, 05 May 2000 22:37:04 +0200 | wenzelm | use Sign.simple_read_term; | file | diff | annotate |
| Mon, 13 Mar 2000 13:28:31 +0100 | wenzelm | adapted to new PureThy.add_thms etc.; | file | diff | annotate |
| Thu, 13 Jan 2000 17:34:39 +0100 | paulson | change in add_thmss to suppress warning | file | diff | annotate |
| Mon, 04 Oct 1999 21:39:36 +0200 | wenzelm | tuned; | file | diff | annotate |
| Wed, 27 Jan 1999 15:58:22 +0100 | paulson | automatic insertion of datatype intr rules into claset | file | diff | annotate |
| Tue, 19 Jan 1999 11:18:11 +0100 | paulson | removal of the (thm list) argument of mk_cases | file | diff | annotate |
| Wed, 13 Jan 1999 11:57:09 +0100 | paulson | datatype package improvements | file | diff | annotate |
| Tue, 12 Jan 1999 15:17:37 +0100 | wenzelm | eliminated global/local names; | file | diff | annotate |
| Tue, 12 Jan 1999 13:54:51 +0100 | wenzelm | eliminated tthm type and Attribute structure; | file | diff | annotate |
| Thu, 07 Jan 1999 18:30:55 +0100 | paulson | ZF: the natural numbers as a datatype | file | diff | annotate |
| Wed, 06 Jan 1999 13:24:33 +0100 | paulson | induct_tac and exhaust_tac | file | diff | annotate |
| Mon, 28 Dec 1998 16:58:11 +0100 | paulson | revised datatype definition package | file | diff | annotate |