| Thu, 03 Apr 1997 09:46:42 +0200 |
nipkow |
Removed (Unit) in Prod.
|
file |
diff |
annotate
|
| Thu, 28 Nov 1996 12:31:33 +0100 |
paulson |
Replaced map...~~ by ListPair.map
|
file |
diff |
annotate
|
| Thu, 26 Sep 1996 12:47:47 +0200 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
| Fri, 02 Aug 1996 12:14:49 +0200 |
berghofe |
Replaced prove_case_cong by Konrad Slinds optimized version.
|
file |
diff |
annotate
|
| Tue, 18 Jun 1996 16:17:38 +0200 |
paulson |
Translation infixes <->, etc., no longer available at top-level
|
file |
diff |
annotate
|
| Fri, 26 Apr 1996 12:33:30 +0200 |
clasohm |
added changes by Konrad to prove_nchotomy
|
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
|
| Tue, 30 Jan 1996 15:24:36 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Mon, 29 Jan 1996 13:48:37 +0100 |
clasohm |
changed the way simpsets and information about datatypes are stored
|
file |
diff |
annotate
|
| Tue, 21 Nov 1995 14:53:03 +0100 |
clasohm |
added call of store_datatype
|
file |
diff |
annotate
|
| Wed, 11 Oct 1995 11:22:35 +0100 |
nipkow |
All constants introduced by datatype now operate on class term explicitly.
|
file |
diff |
annotate
|
| Thu, 30 Mar 1995 13:07:59 +0200 |
clasohm |
removed unnecessary parentheses from the generated rules
|
file |
diff |
annotate
|
| Fri, 17 Mar 1995 22:46:26 +0100 |
clasohm |
fixed two severe bugs in calc_xrules and case_rule
|
file |
diff |
annotate
|
| Fri, 03 Mar 1995 12:02:25 +0100 |
clasohm |
new version of HOL with curried function application
|
file |
diff |
annotate
|