src/ZF/Constructible/L_axioms.thy
changeset 13418 7c0ba9dba978
parent 13385 31df66ca0780
child 13428 99e52e78eb65
     1.1 --- a/src/ZF/Constructible/L_axioms.thy	Wed Jul 24 16:16:44 2002 +0200
     1.2 +++ b/src/ZF/Constructible/L_axioms.thy	Wed Jul 24 17:59:12 2002 +0200
     1.3 @@ -96,9 +96,7 @@
     1.4         ([transL, nonempty, upair_ax, Union_ax, power_ax, replacement, L_nat] 
     1.5          MRS (inst "M" "L" th));
     1.6  
     1.7 -bind_thm ("ball_abs", triv_axioms_L (thm "M_triv_axioms.ball_abs"));
     1.8  bind_thm ("rall_abs", triv_axioms_L (thm "M_triv_axioms.rall_abs"));
     1.9 -bind_thm ("bex_abs", triv_axioms_L (thm "M_triv_axioms.bex_abs"));
    1.10  bind_thm ("rex_abs", triv_axioms_L (thm "M_triv_axioms.rex_abs"));
    1.11  bind_thm ("ball_iff_equiv", triv_axioms_L (thm "M_triv_axioms.ball_iff_equiv"));
    1.12  bind_thm ("M_equalityI", triv_axioms_L (thm "M_triv_axioms.M_equalityI"));
    1.13 @@ -144,9 +142,7 @@
    1.14  bind_thm ("number3_abs", triv_axioms_L (thm "M_triv_axioms.number3_abs"));
    1.15  *}
    1.16  
    1.17 -declare ball_abs [simp] 
    1.18  declare rall_abs [simp] 
    1.19 -declare bex_abs [simp] 
    1.20  declare rex_abs [simp] 
    1.21  declare empty_abs [simp] 
    1.22  declare subset_abs [simp]