nonterminals;
authorwenzelm
Wed Apr 29 11:41:08 1998 +0200 (1998-04-29)
changeset 4868843a9f5b3c3d
parent 4867 9be2bf0ce909
child 4869 f3d30c02c1db
nonterminals;
tuned setup;
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Wed Apr 29 11:40:37 1998 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Apr 29 11:41:08 1998 +0200
     1.3 @@ -77,7 +77,7 @@
     1.4  
     1.5  (** Additional concrete syntax **)
     1.6  
     1.7 -types
     1.8 +nonterminals
     1.9    letbinds  letbind
    1.10    case_syn  cases_syn
    1.11  
    1.12 @@ -186,17 +186,20 @@
    1.13    arbitrary_def "False ==> arbitrary == (@x. False)"
    1.14  
    1.15  
    1.16 +
    1.17 +(** initial HOL theory setup **)
    1.18 +
    1.19 +setup Simplifier.setup
    1.20 +setup ClasetThyData.setup
    1.21 +setup ThyData.setup
    1.22 +
    1.23 +
    1.24  end
    1.25  
    1.26  
    1.27  ML
    1.28  
    1.29  
    1.30 -(** initial HOL theory setup **)
    1.31 -
    1.32 -val thy_setup = [Simplifier.setup, ClasetThyData.setup, ThyData.setup];
    1.33 -
    1.34 -
    1.35  (** Choice between the HOL and Isabelle style of quantifiers **)
    1.36  
    1.37  val HOL_quantifiers = ref true;