src/HOL/HOL.thy
changeset 4793 03fd006fb97b
parent 4371 8755cdbbf6b3
child 4868 843a9f5b3c3d
     1.1 --- a/src/HOL/HOL.thy	Sat Apr 04 12:26:47 1998 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sat Apr 04 12:28:39 1998 +0200
     1.3 @@ -191,6 +191,12 @@
     1.4  
     1.5  ML
     1.6  
     1.7 +
     1.8 +(** initial HOL theory setup **)
     1.9 +
    1.10 +val thy_setup = [Simplifier.setup, ClasetThyData.setup, ThyData.setup];
    1.11 +
    1.12 +
    1.13  (** Choice between the HOL and Isabelle style of quantifiers **)
    1.14  
    1.15  val HOL_quantifiers = ref true;
    1.16 @@ -207,8 +213,3 @@
    1.17  
    1.18  val print_ast_translation =
    1.19    map alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")];
    1.20 -
    1.21 -
    1.22 -(** HOL theory data **)
    1.23 -
    1.24 -val thy_data = ThyData.hol_data;