| Wed, 27 May 1998 12:21:39 +0200 |
paulson |
Changed require to requires for MLWorks
|
file |
diff |
annotate
|
| Wed, 29 Apr 1998 11:45:16 +0200 |
wenzelm |
Theory.require;
|
file |
diff |
annotate
|
| Mon, 09 Feb 1998 18:09:35 +0100 |
nipkow |
Replaced ALLNEWSUBGOALS by THEN_ALL_NEW
|
file |
diff |
annotate
|
| Fri, 09 Jan 1998 14:02:09 +0100 |
wenzelm |
eliminated make_ord;
|
file |
diff |
annotate
|
| Fri, 19 Dec 1997 10:27:23 +0100 |
wenzelm |
adapted to new sort function;
|
file |
diff |
annotate
|
| Fri, 07 Nov 1997 18:02:15 +0100 |
oheimb |
changed libraray function find to find_index_eq, currying it
|
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:15:08 +0100 |
wenzelm |
adapted to new datatypes thy info;
|
file |
diff |
annotate
|
| Thu, 30 Oct 1997 11:43:32 +0100 |
wenzelm |
PureThy.add_store_defs_i, PureThy.add_store_axioms;
|
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
|
| Thu, 23 Oct 1997 12:48:48 +0200 |
wenzelm |
Sign.name_of;
|
file |
diff |
annotate
|
| Mon, 20 Oct 1997 11:14:55 +0200 |
wenzelm |
adapted to qualified names;
|
file |
diff |
annotate
|
| Fri, 10 Oct 1997 19:02:28 +0200 |
wenzelm |
fixed dots;
|
file |
diff |
annotate
|
| Mon, 06 Oct 1997 19:13:29 +0200 |
wenzelm |
TODO: handle internal / external names;
|
file |
diff |
annotate
|
| Wed, 01 Oct 1997 18:13:41 +0200 |
wenzelm |
fully qualified names: Theory.add_XXX;
|
file |
diff |
annotate
|
| Wed, 06 Aug 1997 01:13:46 +0200 |
berghofe |
Moved some functions which used to be part of thy_data.ML
|
file |
diff |
annotate
|
| Wed, 23 Jul 1997 11:52:22 +0200 |
paulson |
Now Datatype.occs_in_prems prints the necessary warning ITSELF.
|
file |
diff |
annotate
|
| Tue, 22 Jul 1997 11:14:18 +0200 |
paulson |
Removal of the tactical STATE
|
file |
diff |
annotate
|
| 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
|