src/ZF/Constructible/Relative.thy
changeset 21233 5a5c8ea5f66a
parent 16417 9bc16273c2d4
child 21404 eb85850d3eb7
     1.1 --- a/src/ZF/Constructible/Relative.thy	Tue Nov 07 19:39:54 2006 +0100
     1.2 +++ b/src/ZF/Constructible/Relative.thy	Tue Nov 07 19:40:13 2006 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  subsection{* Relativized versions of standard set-theoretic concepts *}
     1.6  
     1.7 -constdefs
     1.8 +definition
     1.9    empty :: "[i=>o,i] => o"
    1.10      "empty(M,z) == \<forall>x[M]. x \<notin> z"
    1.11  
    1.12 @@ -236,7 +236,7 @@
    1.13  
    1.14  
    1.15  subsection {*The relativized ZF axioms*}
    1.16 -constdefs
    1.17 +definition
    1.18  
    1.19    extensionality :: "(i=>o) => o"
    1.20      "extensionality(M) ==
    1.21 @@ -441,7 +441,7 @@
    1.22  
    1.23  
    1.24  text{*More constants, for order types*}
    1.25 -constdefs
    1.26 +definition
    1.27  
    1.28    order_isomorphism :: "[i=>o,i,i,i,i,i] => o"
    1.29      "order_isomorphism(M,A,r,B,s,f) ==
    1.30 @@ -712,7 +712,7 @@
    1.31  
    1.32  subsubsection {*Absoluteness for @{term Lambda}*}
    1.33  
    1.34 -constdefs
    1.35 +definition
    1.36   is_lambda :: "[i=>o, i, [i,i]=>o, i] => o"
    1.37      "is_lambda(M, A, is_b, z) ==
    1.38         \<forall>p[M]. p \<in> z <->
    1.39 @@ -893,7 +893,7 @@
    1.40  	   (\<lambda>x\<in>nat. if (\<exists>y[M]. natnumber_aux(M,n)`y=1 & successor(M,y,x))
    1.41  		     then 1 else 0)"
    1.42  
    1.43 -  constdefs
    1.44 +  definition
    1.45      natnumber :: "[i=>o,i,i] => o"
    1.46        "natnumber(M,n,x) == natnumber_aux(M,n)`x = 1"
    1.47  
    1.48 @@ -1312,7 +1312,7 @@
    1.49  
    1.50  subsection{*Relativization and Absoluteness for Boolean Operators*}
    1.51  
    1.52 -constdefs
    1.53 +definition
    1.54    is_bool_of_o :: "[i=>o, o, i] => o"
    1.55     "is_bool_of_o(M,P,z) == (P & number1(M,z)) | (~P & empty(M,z))"
    1.56  
    1.57 @@ -1365,7 +1365,7 @@
    1.58  
    1.59  subsection{*Relativization and Absoluteness for List Operators*}
    1.60  
    1.61 -constdefs
    1.62 +definition
    1.63  
    1.64    is_Nil :: "[i=>o, i] => o"
    1.65       --{* because @{term "[] \<equiv> Inl(0)"}*}
    1.66 @@ -1390,7 +1390,7 @@
    1.67  by (simp add: is_Cons_def Cons_def)
    1.68  
    1.69  
    1.70 -constdefs
    1.71 +definition
    1.72  
    1.73    quasilist :: "i => o"
    1.74      "quasilist(xs) == xs=Nil | (\<exists>x l. xs = Cons(x,l))"