src/ZF/Constructible/Rec_Separation.thy
changeset 13387 b7464ca2ebbb
parent 13386 f3e9e8b21aba
child 13395 4eb948d1eb4e
     1.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Wed Jul 17 16:41:32 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Thu Jul 18 10:37:55 2002 +0200
     1.3 @@ -996,4 +996,26 @@
     1.4  text{*NB The proofs for type @{term formula} are virtually identical to those
     1.5  for @{term "list(A)"}.  It was a cut-and-paste job! *}
     1.6  
     1.7 +
     1.8 +subsubsection{*Instantiating the locale @{text M_datatypes}*}
     1.9 +ML
    1.10 +{*
    1.11 +val list_replacement1 = thm "list_replacement1"; 
    1.12 +val list_replacement2 = thm "list_replacement2";
    1.13 +val formula_replacement1 = thm "formula_replacement1";
    1.14 +val formula_replacement2 = thm "formula_replacement2";
    1.15 +
    1.16 +val m_datatypes = [list_replacement1, list_replacement2, 
    1.17 +                   formula_replacement1, formula_replacement2];
    1.18 +
    1.19 +fun datatypes_L th =
    1.20 +    kill_flex_triv_prems (m_datatypes MRS (wfrank_L th));
    1.21 +
    1.22 +bind_thm ("list_closed", datatypes_L (thm "M_datatypes.list_closed"));
    1.23 +bind_thm ("formula_closed", datatypes_L (thm "M_datatypes.formula_closed"));
    1.24 +*}
    1.25 +
    1.26 +declare list_closed [intro,simp]
    1.27 +declare formula_closed [intro,simp]
    1.28 +
    1.29  end