| Fri, 18 Jul 1997 13:55:09 +0200 |
wenzelm |
renamed |-> <-| <-> to Parse/PrintRule;
|
file |
diff |
annotate
|
| Fri, 23 May 1997 09:17:26 +0200 |
nipkow |
Added overloaded function `size' for all datatypes.
|
file |
diff |
annotate
|
| Thu, 22 May 1997 13:05:52 +0200 |
nipkow |
Added rotation to exhaust_tac.
|
file |
diff |
annotate
|
| Thu, 22 May 1997 09:20:28 +0200 |
nipkow |
Added exhaustion thm and exhaust_tac for each datatype.
|
file |
diff |
annotate
|
| Wed, 21 May 1997 10:09:21 +0200 |
nipkow |
Replaced Konrad's own add_term_names by the predefined one.
|
file |
diff |
annotate
|
| Thu, 15 May 1997 12:54:30 +0200 |
paulson |
Improved error message in "require_thy"
|
file |
diff |
annotate
|
| Tue, 06 May 1997 13:33:33 +0200 |
nipkow |
Stupid bug in induct_tac caused warning to always appear.
|
file |
diff |
annotate
|
| Mon, 05 May 1997 18:09:31 +0200 |
nipkow |
Cosmetic update of induct_tac; test first now.
|
file |
diff |
annotate
|
| Thu, 24 Apr 1997 18:06:46 +0200 |
nipkow |
Introduced a generic "induct_tac" which picks up the right induction scheme
|
file |
diff |
annotate
|
| 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
|