src/ZF/Constructible/L_axioms.thy
changeset 13505 52a16cb7fefb
parent 13496 6f0c57def6d5
child 13506 acc18a5d2b1a
     1.1 --- a/src/ZF/Constructible/L_axioms.thy	Fri Aug 16 12:48:49 2002 +0200
     1.2 +++ b/src/ZF/Constructible/L_axioms.thy	Fri Aug 16 16:41:48 2002 +0200
     1.3 @@ -1,3 +1,8 @@
     1.4 +(*  Title:      ZF/Constructible/L_axioms.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   2002  University of Cambridge
     1.8 +*)
     1.9  
    1.10  header {* The ZF Axioms (Except Separation) in L *}
    1.11  
    1.12 @@ -1079,7 +1084,7 @@
    1.13      ==> sats(A, function_fm(x), env) <-> is_function(**A, nth(x,env))"
    1.14  by (simp add: function_fm_def is_function_def)
    1.15  
    1.16 -lemma function_iff_sats:
    1.17 +lemma is_function_iff_sats:
    1.18        "[| nth(i,env) = x; nth(j,env) = y;
    1.19            i \<in> nat; env \<in> list(A)|]
    1.20         ==> is_function(**A, x) <-> sats(A, function_fm(i), env)"
    1.21 @@ -1141,11 +1146,11 @@
    1.22  lemmas function_iff_sats =
    1.23          empty_iff_sats number1_iff_sats
    1.24          upair_iff_sats pair_iff_sats union_iff_sats
    1.25 -        cons_iff_sats successor_iff_sats
    1.26 +        big_union_iff_sats cons_iff_sats successor_iff_sats
    1.27          fun_apply_iff_sats  Memrel_iff_sats
    1.28          pred_set_iff_sats domain_iff_sats range_iff_sats field_iff_sats
    1.29          image_iff_sats pre_image_iff_sats
    1.30 -        relation_iff_sats function_iff_sats
    1.31 +        relation_iff_sats is_function_iff_sats
    1.32  
    1.33  
    1.34  theorem typed_function_reflection: