deglobalization
authorhaftmann
Wed Aug 18 12:19:27 2010 +0200 (2010-08-18)
changeset 38514bd9c4e8281ec
parent 38513 33ab01218ae1
child 38521 c9f2b1a91276
child 38522 de7984a7172b
deglobalization
src/ZF/Inductive_ZF.thy
src/ZF/Sum.thy
src/ZF/Tools/primrec_package.ML
src/ZF/ZF.thy
src/ZF/ind_syntax.ML
     1.1 --- a/src/ZF/Inductive_ZF.thy	Wed Aug 18 12:08:21 2010 +0200
     1.2 +++ b/src/ZF/Inductive_ZF.thy	Wed Aug 18 12:19:27 2010 +0200
     1.3 @@ -31,8 +31,8 @@
     1.4  lemma refl_thin: "!!P. a = a ==> P ==> P" .
     1.5  
     1.6  use "ind_syntax.ML"
     1.7 +use "Tools/ind_cases.ML"
     1.8  use "Tools/cartprod.ML"
     1.9 -use "Tools/ind_cases.ML"
    1.10  use "Tools/inductive_package.ML"
    1.11  use "Tools/induct_tacs.ML"
    1.12  use "Tools/primrec_package.ML"
     2.1 --- a/src/ZF/Sum.thy	Wed Aug 18 12:08:21 2010 +0200
     2.2 +++ b/src/ZF/Sum.thy	Wed Aug 18 12:19:27 2010 +0200
     2.3 @@ -9,8 +9,6 @@
     2.4  
     2.5  text{*And the "Part" primitive for simultaneous recursive type definitions*}
     2.6  
     2.7 -global
     2.8 -
     2.9  definition sum :: "[i,i]=>i" (infixr "+" 65) where
    2.10       "A+B == {0}*A Un {1}*B"
    2.11  
    2.12 @@ -27,8 +25,6 @@
    2.13  definition Part :: "[i,i=>i] => i" where
    2.14       "Part(A,h) == {x: A. EX z. x = h(z)}"
    2.15  
    2.16 -local
    2.17 -
    2.18  subsection{*Rules for the @{term Part} Primitive*}
    2.19  
    2.20  lemma Part_iff: 
     3.1 --- a/src/ZF/Tools/primrec_package.ML	Wed Aug 18 12:08:21 2010 +0200
     3.2 +++ b/src/ZF/Tools/primrec_package.ML	Wed Aug 18 12:19:27 2010 +0200
     3.3 @@ -115,8 +115,8 @@
     3.4              case AList.lookup (op =) eqns cname of
     3.5                  NONE => (warning ("no equation for constructor " ^ cname ^
     3.6                                    "\nin definition of function " ^ fname);
     3.7 -                         (Const ("0", Ind_Syntax.iT),
     3.8 -                          #2 recursor_pair, Const ("0", Ind_Syntax.iT)))
     3.9 +                         (Const (@{const_name 0}, Ind_Syntax.iT),
    3.10 +                          #2 recursor_pair, Const (@{const_name 0}, Ind_Syntax.iT)))
    3.11                | SOME (rhs, cargs', eq) =>
    3.12                      (rhs, inst_recursor (recursor_pair, cargs'), eq)
    3.13            val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs))
     4.1 --- a/src/ZF/ZF.thy	Wed Aug 18 12:08:21 2010 +0200
     4.2 +++ b/src/ZF/ZF.thy	Wed Aug 18 12:19:27 2010 +0200
     4.3 @@ -12,8 +12,6 @@
     4.4  
     4.5  ML {* Unsynchronized.reset eta_contract *}
     4.6  
     4.7 -global
     4.8 -
     4.9  typedecl i
    4.10  arities  i :: "term"
    4.11  
    4.12 @@ -209,8 +207,6 @@
    4.13    subset_def:    "A <= B == \<forall>x\<in>A. x\<in>B"
    4.14  
    4.15  
    4.16 -local
    4.17 -
    4.18  axioms
    4.19  
    4.20    (* ZF axioms -- see Suppes p.238
     5.1 --- a/src/ZF/ind_syntax.ML	Wed Aug 18 12:08:21 2010 +0200
     5.2 +++ b/src/ZF/ind_syntax.ML	Wed Aug 18 12:19:27 2010 +0200
     5.3 @@ -18,7 +18,7 @@
     5.4  
     5.5  (** Abstract syntax definitions for ZF **)
     5.6  
     5.7 -val iT = Type("i",[]);
     5.8 +val iT = Type(@{type_name i}, []);
     5.9  
    5.10  (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
    5.11  fun mk_all_imp (A,P) =