removed mk_prodT, mk_not (cf. HOL/hologic.ML);
authorwenzelm
Thu Jul 14 19:28:25 2005 +0200 (2005-07-14)
changeset 168438ff9a80f3c93
parent 16842 5979c46853d1
child 16844 60ab395e6da5
removed mk_prodT, mk_not (cf. HOL/hologic.ML);
tuned;
src/HOLCF/holcf_logic.ML
     1.1 --- a/src/HOLCF/holcf_logic.ML	Thu Jul 14 19:28:24 2005 +0200
     1.2 +++ b/src/HOLCF/holcf_logic.ML	Thu Jul 14 19:28:25 2005 +0200
     1.3 @@ -10,52 +10,45 @@
     1.4  signature HOLCF_LOGIC =
     1.5  sig
     1.6    val mk_btyp: string -> typ * typ -> typ
     1.7 -  val mk_prodT:          typ * typ -> typ
     1.8 -  val mk_not:  term -> term
     1.9 -
    1.10 -  val HOLCF_sg: Sign.sg
    1.11    val pcpoC: class
    1.12    val pcpoS: sort
    1.13    val mk_TFree: string -> typ
    1.14    val cfun_arrow: string
    1.15 -  val ->>      : typ * typ -> typ
    1.16 -  val mk_ssumT : typ * typ -> typ
    1.17 +  val ->> : typ * typ -> typ
    1.18 +  val mk_ssumT: typ * typ -> typ
    1.19    val mk_sprodT: typ * typ -> typ
    1.20    val mk_uT: typ -> typ
    1.21    val trT: typ
    1.22    val oneT: typ
    1.23 -
    1.24  end;
    1.25  
    1.26 -
    1.27  structure HOLCFLogic: HOLCF_LOGIC =
    1.28  struct
    1.29  
    1.30 -open HOLogic;
    1.31 +(* sort pcpo *)
    1.32 +
    1.33 +val pcpoC = Sign.intern_class (the_context ()) "pcpo";
    1.34 +val pcpoS = [pcpoC];
    1.35 +fun mk_TFree s = TFree ("'" ^ s, pcpoS);
    1.36 +
    1.37 +
    1.38 +(* basic types *)
    1.39  
    1.40  fun mk_btyp t (S,T) = Type (t,[S,T]);
    1.41 -val mk_prodT = mk_btyp "*";
    1.42  
    1.43 -fun mk_not P  = Const ("Not", boolT --> boolT) $ P;
    1.44 -
    1.45 -(* basics *)
    1.46 -
    1.47 -val HOLCF_sg    = sign_of HOLCF.thy;
    1.48 -val pcpoC       = Sign.intern_class HOLCF_sg "pcpo";
    1.49 -val pcpoS       = [pcpoC];
    1.50 -fun mk_TFree s  = TFree ("'"^s, pcpoS);
    1.51 +local
    1.52 +  val intern_type = Sign.intern_type (the_context ());
    1.53 +  val u = intern_type "u";
    1.54 +in
    1.55  
    1.56 -(*cfun, ssum, sprod, u, tr, one *)
    1.57 +val cfun_arrow = intern_type "->";
    1.58 +val op ->> = mk_btyp cfun_arrow;
    1.59 +val mk_ssumT = mk_btyp (intern_type "++");
    1.60 +val mk_sprodT = mk_btyp (intern_type "**");
    1.61 +fun mk_uT T = Type (u, [T]);
    1.62 +val trT = Type (intern_type "tr" , []);
    1.63 +val oneT = Type (intern_type "one", []);
    1.64  
    1.65 -local val intern = Sign.intern_type HOLCF_sg;
    1.66 -in
    1.67 -val cfun_arrow = intern "->";
    1.68 -val op   ->>  = mk_btyp cfun_arrow;
    1.69 -val mk_ssumT  = mk_btyp (intern "++");
    1.70 -val mk_sprodT = mk_btyp (intern "**");
    1.71 -fun mk_uT T   = Type (intern "u"  ,[T]);
    1.72 -val trT       = Type (intern "tr" ,[ ]);
    1.73 -val oneT      = Type (intern "one",[ ]);
    1.74  end;
    1.75  
    1.76  end;