src/ZF/ex/Mutil.thy
changeset 6117 f9aad8ccd590
parent 1806 12708740f58d
child 11316 b4e71bd751e4
     1.1 --- a/src/ZF/ex/Mutil.thy	Wed Jan 13 12:44:33 1999 +0100
     1.2 +++ b/src/ZF/ex/Mutil.thy	Wed Jan 13 15:14:47 1999 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4    intrs
     1.5      horiz  "[| i: nat;  j: nat |] ==> {<i,j>, <i,succ(j)>} : domino"
     1.6      vertl  "[| i: nat;  j: nat |] ==> {<i,j>, <succ(i),j>} : domino"
     1.7 -  type_intrs "[empty_subsetI, cons_subsetI, PowI, SigmaI, nat_succI]"
     1.8 +  type_intrs  empty_subsetI, cons_subsetI, PowI, SigmaI, nat_succI
     1.9  
    1.10  
    1.11  inductive
    1.12 @@ -26,7 +26,7 @@
    1.13    intrs
    1.14      empty  "0 : tiling(A)"
    1.15      Un     "[| a: A;  t: tiling(A);  a Int t = 0 |] ==> a Un t : tiling(A)"
    1.16 -  type_intrs "[empty_subsetI, Union_upper, Un_least, PowI]"
    1.17 +  type_intrs  empty_subsetI, Union_upper, Un_least, PowI
    1.18    type_elims "[make_elim PowD]"
    1.19  
    1.20  constdefs