--- a/src/ZF/Inductive_ZF.thy Wed Aug 18 12:08:21 2010 +0200
+++ b/src/ZF/Inductive_ZF.thy Wed Aug 18 12:19:27 2010 +0200
@@ -31,8 +31,8 @@
lemma refl_thin: "!!P. a = a ==> P ==> P" .
use "ind_syntax.ML"
+use "Tools/ind_cases.ML"
use "Tools/cartprod.ML"
-use "Tools/ind_cases.ML"
use "Tools/inductive_package.ML"
use "Tools/induct_tacs.ML"
use "Tools/primrec_package.ML"
--- a/src/ZF/Sum.thy Wed Aug 18 12:08:21 2010 +0200
+++ b/src/ZF/Sum.thy Wed Aug 18 12:19:27 2010 +0200
@@ -9,8 +9,6 @@
text{*And the "Part" primitive for simultaneous recursive type definitions*}
-global
-
definition sum :: "[i,i]=>i" (infixr "+" 65) where
"A+B == {0}*A Un {1}*B"
@@ -27,8 +25,6 @@
definition Part :: "[i,i=>i] => i" where
"Part(A,h) == {x: A. EX z. x = h(z)}"
-local
-
subsection{*Rules for the @{term Part} Primitive*}
lemma Part_iff:
--- a/src/ZF/Tools/primrec_package.ML Wed Aug 18 12:08:21 2010 +0200
+++ b/src/ZF/Tools/primrec_package.ML Wed Aug 18 12:19:27 2010 +0200
@@ -115,8 +115,8 @@
case AList.lookup (op =) eqns cname of
NONE => (warning ("no equation for constructor " ^ cname ^
"\nin definition of function " ^ fname);
- (Const ("0", Ind_Syntax.iT),
- #2 recursor_pair, Const ("0", Ind_Syntax.iT)))
+ (Const (@{const_name 0}, Ind_Syntax.iT),
+ #2 recursor_pair, Const (@{const_name 0}, Ind_Syntax.iT)))
| SOME (rhs, cargs', eq) =>
(rhs, inst_recursor (recursor_pair, cargs'), eq)
val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs))
--- a/src/ZF/ZF.thy Wed Aug 18 12:08:21 2010 +0200
+++ b/src/ZF/ZF.thy Wed Aug 18 12:19:27 2010 +0200
@@ -12,8 +12,6 @@
ML {* Unsynchronized.reset eta_contract *}
-global
-
typedecl i
arities i :: "term"
@@ -209,8 +207,6 @@
subset_def: "A <= B == \<forall>x\<in>A. x\<in>B"
-local
-
axioms
(* ZF axioms -- see Suppes p.238
--- a/src/ZF/ind_syntax.ML Wed Aug 18 12:08:21 2010 +0200
+++ b/src/ZF/ind_syntax.ML Wed Aug 18 12:19:27 2010 +0200
@@ -18,7 +18,7 @@
(** Abstract syntax definitions for ZF **)
-val iT = Type("i",[]);
+val iT = Type(@{type_name i}, []);
(*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
fun mk_all_imp (A,P) =