| Thu, 30 Jul 1998 23:14:41 +0200 |
berghofe |
Fixed primrec.
|
file |
diff |
annotate
|
| Thu, 30 Jul 1998 22:58:05 +0200 |
berghofe |
Fixed primrec.
|
file |
diff |
annotate
|
| Thu, 30 Jul 1998 17:59:57 +0200 |
wenzelm |
fixed primrec;
|
file |
diff |
annotate
|
| Fri, 24 Jul 1998 13:03:20 +0200 |
berghofe |
Adapted to new datatype package.
|
file |
diff |
annotate
|
| Tue, 30 Jun 1998 20:42:47 +0200 |
berghofe |
Adapted to new inductive definition package.
|
file |
diff |
annotate
|
| Wed, 29 Apr 1998 11:44:30 +0200 |
wenzelm |
TypedefPackage.add_typedef;
|
file |
diff |
annotate
|
| Thu, 08 Jan 1998 18:09:47 +0100 |
oheimb |
added split_paired_Ex to the implicit simpset
|
file |
diff |
annotate
|
| Thu, 13 Nov 1997 15:14:14 +0100 |
wenzelm |
fixed record parser;
|
file |
diff |
annotate
|
| Thu, 13 Nov 1997 12:43:17 +0100 |
wenzelm |
improved record syntax;
|
file |
diff |
annotate
|
| Wed, 12 Nov 1997 12:24:55 +0100 |
oheimb |
renamed split_T_case_prem to split_T_case_asm
|
file |
diff |
annotate
|
| Fri, 07 Nov 1997 08:25:02 +0100 |
nipkow |
Each datatype t now proves a theorem split_t_case_prem
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 21:13:24 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 12:24:13 +0100 |
wenzelm |
isatool fixclasimp;
|
file |
diff |
annotate
|
| Thu, 30 Oct 1997 09:45:03 +0100 |
nipkow |
For each datatype `t' there is now a theorem `split_t_case' of the form
|
file |
diff |
annotate
|
| Fri, 24 Oct 1997 17:28:20 +0200 |
wenzelm |
record: tuned output;
|
file |
diff |
annotate
|
| Thu, 23 Oct 1997 12:49:16 +0200 |
wenzelm |
added record section;
|
file |
diff |
annotate
|
| Mon, 20 Oct 1997 11:14:55 +0200 |
wenzelm |
adapted to qualified names;
|
file |
diff |
annotate
|
| Wed, 10 Sep 1997 14:18:12 +0200 |
nipkow |
Added Larry's test for preventing a datatype shadowing a theory.
|
file |
diff |
annotate
|
| Wed, 06 Aug 1997 11:57:52 +0200 |
wenzelm |
use ThySyn.add_syntax;
|
file |
diff |
annotate
|
| Wed, 06 Aug 1997 01:18:31 +0200 |
berghofe |
Replaced "init_thy_reader" by "set_parser".
|
file |
diff |
annotate
|
| Mon, 23 Jun 1997 10:35:49 +0200 |
paulson |
New "congs" keyword for recdef theory section
|
file |
diff |
annotate
|
| Thu, 05 Jun 1997 13:22:25 +0200 |
paulson |
A slight simplification of optstring
|
file |
diff |
annotate
|
| Mon, 26 May 1997 12:42:38 +0200 |
paulson |
Now recdef checks the name of the function being defined.
|
file |
diff |
annotate
|
| Fri, 23 May 1997 09:17:26 +0200 |
nipkow |
Added overloaded function `size' for all datatypes.
|
file |
diff |
annotate
|
| Thu, 15 May 1997 12:53:12 +0200 |
paulson |
TFL theory section
|
file |
diff |
annotate
|
| Thu, 10 Apr 1997 12:20:55 +0200 |
nipkow |
Turned Addsimps into AddIffs for datatype laws.
|
file |
diff |
annotate
|
| Wed, 09 Apr 1997 12:32:04 +0200 |
paulson |
Using Blast_tac
|
file |
diff |
annotate
|
| Fri, 05 Jul 1996 14:22:59 +0200 |
berghofe |
Simplified syntax of primrec definitions.
|
file |
diff |
annotate
|
| Thu, 06 Jun 1996 13:13:18 +0200 |
paulson |
Quotes now optional around inductive set
|
file |
diff |
annotate
|
| Fri, 19 Apr 1996 11:33:24 +0200 |
clasohm |
added Konrad's code for the datatype package
|
file |
diff |
annotate
|
| Wed, 13 Mar 1996 11:55:25 +0100 |
clasohm |
modified primrec so it can be used in MiniML/Type.thy
|
file |
diff |
annotate
|
| Mon, 05 Feb 1996 21:27:16 +0100 |
clasohm |
expanded tabs; renamed subtype to typedef;
|
file |
diff |
annotate
|
| Tue, 30 Jan 1996 15:24:36 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Tue, 02 Jan 1996 10:46:50 +0100 |
paulson |
Improving space efficiency of inductive/datatype definitions.
|
file |
diff |
annotate
|
| Thu, 02 Nov 1995 12:45:58 +0100 |
clasohm |
extended complex_typ
|
file |
diff |
annotate
|
| Wed, 04 Oct 1995 13:10:03 +0100 |
clasohm |
added local simpsets; removed IOA from 'make test'
|
file |
diff |
annotate
|
| Fri, 08 Sep 1995 13:23:04 +0200 |
clasohm |
added nested types on right hand side of datatype definitions
|
file |
diff |
annotate
|
| Tue, 28 Mar 1995 12:25:20 +0200 |
clasohm |
changed syntax of datatype declarations (curried types for constructor
|
file |
diff |
annotate
|
| Fri, 03 Mar 1995 12:02:25 +0100 |
clasohm |
new version of HOL with curried function application
|
file |
diff |
annotate
|