src/ZF/Constructible/Wellorderings.thy
changeset 21233 5a5c8ea5f66a
parent 16417 9bc16273c2d4
child 21404 eb85850d3eb7
     1.1 --- a/src/ZF/Constructible/Wellorderings.thy	Tue Nov 07 19:39:54 2006 +0100
     1.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Tue Nov 07 19:40:13 2006 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4  
     1.5  subsection{*Wellorderings*}
     1.6  
     1.7 -constdefs
     1.8 +definition
     1.9    irreflexive :: "[i=>o,i,i]=>o"
    1.10      "irreflexive(M,A,r) == \<forall>x[M]. x\<in>A --> <x,x> \<notin> r"
    1.11