| Thu, 20 Nov 1997 15:36:09 +0100 |
wenzelm |
adapted print methods;
|
file |
diff |
annotate
|
| Wed, 05 Nov 1997 11:49:07 +0100 |
wenzelm |
tuned record_info;
|
file |
diff |
annotate
|
| Tue, 04 Nov 1997 16:49:35 +0100 |
wenzelm |
tuned 'records' stuff;
|
file |
diff |
annotate
|
| Tue, 04 Nov 1997 14:09:37 +0100 |
narasche |
data kinds 'datatypes', data kinds 'records' added
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 21:12:40 +0100 |
wenzelm |
datatypes;
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 12:04:38 +0100 |
wenzelm |
HOL theory data.
|
file |
diff |
annotate
|
| Tue, 22 Jul 1997 11:14:18 +0200 |
paulson |
Removal of the tactical STATE
|
file |
diff |
annotate
|
| Wed, 09 Jul 1997 17:00:34 +0200 |
wenzelm |
removed obsolete init_pps and init_thy_reader;
|
file |
diff |
annotate
|
| Thu, 22 May 1997 18:29:17 +0200 |
nipkow |
exhaust_tac can now deal with whole terms rather than just variables.
|
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, 24 Apr 1997 18:06:46 +0200 |
nipkow |
Introduced a generic "induct_tac" which picks up the right induction scheme
|
file |
diff |
annotate
|
| Wed, 29 Jan 1997 15:32:18 +0100 |
paulson |
Moved qed_spec_mp, etc., from HOL.ML to thy_data.ML so that they work
|
file |
diff |
annotate
|
| Tue, 07 May 1996 09:58:12 +0200 |
berghofe |
Added function claset_of.
|
file |
diff |
annotate
|
| Fri, 19 Apr 1996 11:33:24 +0200 |
clasohm |
added Konrad's code for the datatype package
|
file |
diff |
annotate
|
| Fri, 12 Apr 1996 12:41:26 +0200 |
clasohm |
changed first parameter of add_thydata and get_thydata
|
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
|