replaced thy_data by thy_setup;
authorwenzelm
Sat Apr 04 12:28:39 1998 +0200 (1998-04-04)
changeset 479303fd006fb97b
parent 4792 8e3c2dddb9c8
child 4794 9db0916ecdae
replaced thy_data by thy_setup;
src/FOL/FOL.thy
src/FOL/IFOL.thy
src/HOL/HOL.thy
     1.1 --- a/src/FOL/FOL.thy	Sat Apr 04 12:26:47 1998 +0200
     1.2 +++ b/src/FOL/FOL.thy	Sat Apr 04 12:28:39 1998 +0200
     1.3 @@ -6,4 +6,4 @@
     1.4  
     1.5  end
     1.6  
     1.7 -ML val thy_data = [ClasetThyData.thy_data];
     1.8 +ML val thy_setup = [ClasetThyData.setup];
     2.1 --- a/src/FOL/IFOL.thy	Sat Apr 04 12:26:47 1998 +0200
     2.2 +++ b/src/FOL/IFOL.thy	Sat Apr 04 12:28:39 1998 +0200
     2.3 @@ -114,4 +114,4 @@
     2.4  end
     2.5  
     2.6  
     2.7 -ML val thy_data = [Simplifier.simpset_thy_data];
     2.8 +ML val thy_setup = [Simplifier.setup];
     3.1 --- a/src/HOL/HOL.thy	Sat Apr 04 12:26:47 1998 +0200
     3.2 +++ b/src/HOL/HOL.thy	Sat Apr 04 12:28:39 1998 +0200
     3.3 @@ -191,6 +191,12 @@
     3.4  
     3.5  ML
     3.6  
     3.7 +
     3.8 +(** initial HOL theory setup **)
     3.9 +
    3.10 +val thy_setup = [Simplifier.setup, ClasetThyData.setup, ThyData.setup];
    3.11 +
    3.12 +
    3.13  (** Choice between the HOL and Isabelle style of quantifiers **)
    3.14  
    3.15  val HOL_quantifiers = ref true;
    3.16 @@ -207,8 +213,3 @@
    3.17  
    3.18  val print_ast_translation =
    3.19    map alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")];
    3.20 -
    3.21 -
    3.22 -(** HOL theory data **)
    3.23 -
    3.24 -val thy_data = ThyData.hol_data;