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))"
```