src/ZF/ex/Ntree.thy
changeset 6117 f9aad8ccd590
parent 1478 2b8c2a7547ab
child 8125 df502e820d07
     1.1 --- a/src/ZF/ex/Ntree.thy	Wed Jan 13 12:44:33 1999 +0100
     1.2 +++ b/src/ZF/ex/Ntree.thy	Wed Jan 13 15:14:47 1999 +0100
     1.3 @@ -19,16 +19,16 @@
     1.4    "ntree(A)" = Branch ("a: A", "h: (UN n:nat. n -> ntree(A))")
     1.5    monos       "[[subset_refl, Pi_mono] MRS UN_mono]"    (*MUST have this form*)
     1.6    type_intrs  "[nat_fun_univ RS subsetD]"
     1.7 -  type_elims  "[UN_E]"
     1.8 +  type_elims   UN_E
     1.9  
    1.10  datatype
    1.11    "maptree(A)" = Sons ("a: A", "h: maptree(A) -||> maptree(A)")
    1.12 -  monos       "[FiniteFun_mono1]"       (*Use monotonicity in BOTH args*)
    1.13 +  monos        FiniteFun_mono1         (*Use monotonicity in BOTH args*)
    1.14    type_intrs  "[FiniteFun_univ1 RS subsetD]"
    1.15  
    1.16  datatype
    1.17    "maptree2(A,B)" = Sons2 ("a: A", "h: B -||> maptree2(A,B)")
    1.18    monos       "[subset_refl RS FiniteFun_mono]"
    1.19 -  type_intrs  "[FiniteFun_in_univ']"
    1.20 +  type_intrs   FiniteFun_in_univ'
    1.21  
    1.22  end