# HG changeset patch
# User paulson
# Date 971428556 -7200
# Node ID e928bdf62014555829696347523f323cce5356f0
# Parent  1ead773b365ee795c9b32af8b1204e4f25f90f29
renamed fp_Tarski to fp_unfold

diff -r 1ead773b365e -r e928bdf62014 src/ZF/Cardinal.ML
--- a/src/ZF/Cardinal.ML	Fri Oct 13 10:49:05 2000 +0200
+++ b/src/ZF/Cardinal.ML	Fri Oct 13 11:15:56 2000 +0200
@@ -22,7 +22,7 @@
 \    g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) =       \
 \    X - lfp(X, %W. X - g``(Y - f``W)) ";
 by (res_inst_tac [("P", "%u. ?v = X-u")] 
-     (decomp_bnd_mono RS lfp_Tarski RS ssubst) 1);
+     (decomp_bnd_mono RS lfp_unfold RS ssubst) 1);
 by (simp_tac (simpset() addsimps [subset_refl, double_complement,
                              gfun RS fun_is_rel RS image_subset]) 1);
 qed "Banach_last_equation";
diff -r 1ead773b365e -r e928bdf62014 src/ZF/Fixedpt.ML
--- a/src/ZF/Fixedpt.ML	Fri Oct 13 10:49:05 2000 +0200
+++ b/src/ZF/Fixedpt.ML	Fri Oct 13 11:15:56 2000 +0200
@@ -98,14 +98,14 @@
 
 Goal "bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))";
 by (REPEAT (ares_tac [equalityI,lfp_lemma2,lfp_lemma3] 1));
-qed "lfp_Tarski";
+qed "lfp_unfold";
 
 (*Definition form, to control unfolding*)
 val [rew,mono] = goal (the_context ())
     "[| A==lfp(D,h);  bnd_mono(D,h) |] ==> A = h(A)";
 by (rewtac rew);
-by (rtac (mono RS lfp_Tarski) 1);
-qed "def_lfp_Tarski";
+by (rtac (mono RS lfp_unfold) 1);
+qed "def_lfp_unfold";
 
 (*** General induction rule for least fixedpoints ***)
 
@@ -222,14 +222,14 @@
 
 Goal "bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))";
 by (REPEAT (ares_tac [equalityI,gfp_lemma2,gfp_lemma3] 1));
-qed "gfp_Tarski";
+qed "gfp_unfold";
 
 (*Definition form, to control unfolding*)
 val [rew,mono] = goal (the_context ())
     "[| A==gfp(D,h);  bnd_mono(D,h) |] ==> A = h(A)";
 by (rewtac rew);
-by (rtac (mono RS gfp_Tarski) 1);
-qed "def_gfp_Tarski";
+by (rtac (mono RS gfp_unfold) 1);
+qed "def_gfp_unfold";
 
 
 (*** Coinduction rules for greatest fixed points ***)
diff -r 1ead773b365e -r e928bdf62014 src/ZF/IMP/Equiv.ML
--- a/src/ZF/IMP/Equiv.ML	Fri Oct 13 10:49:05 2000 +0200
+++ b/src/ZF/IMP/Equiv.ML	Fri Oct 13 11:15:56 2000 +0200
@@ -53,11 +53,11 @@
 (* comp *)
 by (Fast_tac 1);
 (* while *)
-by (etac (Gamma_bnd_mono RS lfp_Tarski RS ssubst) 1);
+by (etac (Gamma_bnd_mono RS lfp_unfold RS ssubst) 1);
 by (asm_simp_tac (simpset() addsimps [Gamma_def, bexp1]) 1);
 by (blast_tac (claset() addSIs [bexp1]@evalb_type_intrs) 1);
 (* recursive case of while *)
-by (etac (Gamma_bnd_mono RS lfp_Tarski RS ssubst) 1);
+by (etac (Gamma_bnd_mono RS lfp_unfold RS ssubst) 1);
 by (asm_full_simp_tac (simpset() addsimps [Gamma_def, bexp1]) 1);
 by (blast_tac (claset() addSIs [bexp1]@evalb_type_intrs) 1);
 val com1 = result();
diff -r 1ead773b365e -r e928bdf62014 src/ZF/Inductive.ML
--- a/src/ZF/Inductive.ML	Fri Oct 13 10:49:05 2000 +0200
+++ b/src/ZF/Inductive.ML	Fri Oct 13 11:15:56 2000 +0200
@@ -21,7 +21,7 @@
   val bnd_mono  = Const("Fixedpt.bnd_mono", [iT,iT-->iT]--->oT)
   val bnd_monoI = bnd_monoI
   val subs      = def_lfp_subset
-  val Tarski    = def_lfp_Tarski
+  val Tarski    = def_lfp_unfold
   val induct    = def_induct
   end;
 
@@ -68,7 +68,7 @@
   val bnd_mono  = Const("Fixedpt.bnd_mono", [iT,iT-->iT]--->oT)
   val bnd_monoI = bnd_monoI
   val subs      = def_gfp_subset
-  val Tarski    = def_gfp_Tarski
+  val Tarski    = def_gfp_unfold
   val induct    = def_Collect_coinduct
   end;
 
diff -r 1ead773b365e -r e928bdf62014 src/ZF/Nat.ML
--- a/src/ZF/Nat.ML	Fri Oct 13 10:49:05 2000 +0200
+++ b/src/ZF/Nat.ML	Fri Oct 13 11:15:56 2000 +0200
@@ -14,7 +14,7 @@
 qed "nat_bnd_mono";
 
 (* nat = {0} Un {succ(x). x:nat} *)
-bind_thm ("nat_unfold", nat_bnd_mono RS (nat_def RS def_lfp_Tarski));
+bind_thm ("nat_unfold", nat_bnd_mono RS (nat_def RS def_lfp_unfold));
 
 (** Type checking of 0 and successor **)
 
diff -r 1ead773b365e -r e928bdf62014 src/ZF/Trancl.ML
--- a/src/ZF/Trancl.ML	Fri Oct 13 10:49:05 2000 +0200
+++ b/src/ZF/Trancl.ML	Fri Oct 13 11:15:56 2000 +0200
@@ -19,7 +19,7 @@
 qed "rtrancl_mono";
 
 (* r^* = id(field(r)) Un ( r O r^* )    *)
-bind_thm ("rtrancl_unfold", rtrancl_bnd_mono RS (rtrancl_def RS def_lfp_Tarski));
+bind_thm ("rtrancl_unfold", rtrancl_bnd_mono RS (rtrancl_def RS def_lfp_unfold));
 
 (** The relation rtrancl **)
 
diff -r 1ead773b365e -r e928bdf62014 src/ZF/ex/CoUnit.ML
--- a/src/ZF/ex/CoUnit.ML	Fri Oct 13 10:49:05 2000 +0200
+++ b/src/ZF/ex/CoUnit.ML	Fri Oct 13 11:15:56 2000 +0200
@@ -45,7 +45,7 @@
 by (rtac (singletonI RS counit2.coinduct) 1);
 by (rtac (qunivI RS singleton_subsetI) 1);
 by (rtac ([lfp_subset, empty_subsetI RS univ_mono] MRS subset_trans) 1);
-by (fast_tac (claset() addSIs [Con2_bnd_mono RS lfp_Tarski]) 1);
+by (fast_tac (claset() addSIs [Con2_bnd_mono RS lfp_unfold]) 1);
 qed "lfp_Con2_in_counit2";
 
 (*Lemma for proving finality.  Borrowed from ex/llist_eq.ML!*)
diff -r 1ead773b365e -r e928bdf62014 src/ZF/ex/LList.ML
--- a/src/ZF/ex/LList.ML	Fri Oct 13 10:49:05 2000 +0200
+++ b/src/ZF/ex/LList.ML	Fri Oct 13 11:15:56 2000 +0200
@@ -124,7 +124,7 @@
 
 (* lconst(a) = LCons(a,lconst(a)) *)
 bind_thm ("lconst",
-    ([lconst_def, lconst_fun_bnd_mono] MRS def_lfp_Tarski));
+    ([lconst_def, lconst_fun_bnd_mono] MRS def_lfp_unfold));
 
 val lconst_subset = lconst_def RS def_lfp_subset;