--- a/src/HOL/HOL.thy Wed Apr 29 11:40:37 1998 +0200
+++ b/src/HOL/HOL.thy Wed Apr 29 11:41:08 1998 +0200
@@ -77,7 +77,7 @@
(** Additional concrete syntax **)
-types
+nonterminals
letbinds letbind
case_syn cases_syn
@@ -186,17 +186,20 @@
arbitrary_def "False ==> arbitrary == (@x. False)"
+
+(** initial HOL theory setup **)
+
+setup Simplifier.setup
+setup ClasetThyData.setup
+setup ThyData.setup
+
+
end
ML
-(** initial HOL theory setup **)
-
-val thy_setup = [Simplifier.setup, ClasetThyData.setup, ThyData.setup];
-
-
(** Choice between the HOL and Isabelle style of quantifiers **)
val HOL_quantifiers = ref true;