src/ZF/ex/acc.ML
changeset 279 7738aed3f84d
parent 95 2246a80b1cb5
     1.1 --- a/src/ZF/ex/acc.ML	Thu Mar 17 11:24:31 1994 +0100
     1.2 +++ b/src/ZF/ex/acc.ML	Thu Mar 17 12:36:58 1994 +0100
     1.3 @@ -10,13 +10,12 @@
     1.4  *)
     1.5  
     1.6  structure Acc = Inductive_Fun
     1.7 - (val thy = WF.thy addconsts [(["acc"],"i=>i")];
     1.8 -  val rec_doms = [("acc", "field(r)")];
     1.9 -  val sintrs = 
    1.10 -      ["[| r-``{a} : Pow(acc(r));  a : field(r) |] ==> a : acc(r)"];
    1.11 -  val monos = [Pow_mono];
    1.12 -  val con_defs = [];
    1.13 -  val type_intrs = [];
    1.14 + (val thy        = WF.thy addconsts [(["acc"],"i=>i")]
    1.15 +  val rec_doms   = [("acc", "field(r)")]
    1.16 +  val sintrs     = ["[| r-``{a}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"]
    1.17 +  val monos      = [Pow_mono]
    1.18 +  val con_defs   = []
    1.19 +  val type_intrs = []
    1.20    val type_elims = []);
    1.21  
    1.22  goal Acc.thy "!!a b r. [| b: acc(r);  <a,b>: r |] ==> a: acc(r)";