lcp [Fri, 25 Nov 1994 11:10:26 +0100] rev 181
checks that the recursive sets are Consts before taking
them apart! Bug was introduced during the translation to theory sections.
nipkow [Fri, 25 Nov 1994 09:59:51 +0100] rev 180
renamed term_induct/2 -> Term_induct/2
clasohm [Fri, 25 Nov 1994 09:12:16 +0100] rev 179
replaced prove_goal by qed_goal
nipkow [Thu, 24 Nov 1994 20:31:09 +0100] rev 178
rules -> defs
nipkow [Thu, 24 Nov 1994 20:11:40 +0100] rev 177
The collection of theories required for inductive definitions.
nipkow [Thu, 24 Nov 1994 20:00:52 +0100] rev 176
Trancl.{thy,ML} was missing
wenzelm [Wed, 23 Nov 1994 15:09:44 +0100] rev 175
moved parser stuff to thy_syntax.ML;
wenzelm [Wed, 23 Nov 1994 10:41:42 +0100] rev 174
add_subtype now adds constant definition for the representing set;
wenzelm [Wed, 23 Nov 1994 10:37:27 +0100] rev 173
moved remaining thy syntax stuff to thy_syntax.ML;
wenzelm [Wed, 23 Nov 1994 10:36:03 +0100] rev 172
added 'datatype' and 'primrec';
subtype: added axiom <tyname>_def;