src/ZF/Constructible/Relative.thy
changeset 22710 f44439cdce77
parent 21404 eb85850d3eb7
child 32960 69916a850301
     1.1 --- a/src/ZF/Constructible/Relative.thy	Sun Apr 15 23:25:50 2007 +0200
     1.2 +++ b/src/ZF/Constructible/Relative.thy	Sun Apr 15 23:25:52 2007 +0200
     1.3 @@ -1431,12 +1431,12 @@
     1.4  
     1.5  definition
     1.6    is_Nil :: "[i=>o, i] => o" where
     1.7 -     --{* because @{term "[] \<equiv> Inl(0)"}*}
     1.8 +     --{* because @{prop "[] \<equiv> Inl(0)"}*}
     1.9      "is_Nil(M,xs) == \<exists>zero[M]. empty(M,zero) & is_Inl(M,zero,xs)"
    1.10  
    1.11  definition
    1.12    is_Cons :: "[i=>o,i,i,i] => o" where
    1.13 -     --{* because @{term "Cons(a, l) \<equiv> Inr(\<langle>a,l\<rangle>)"}*}
    1.14 +     --{* because @{prop "Cons(a, l) \<equiv> Inr(\<langle>a,l\<rangle>)"}*}
    1.15      "is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)"
    1.16  
    1.17