diff -r 5b12cd0a3b3c -r 9540c2f2ea77 Myhill_1.thy
--- a/Myhill_1.thy	Thu Feb 10 12:32:45 2011 +0000
+++ b/Myhill_1.thy	Thu Feb 10 13:10:16 2011 +0000
@@ -448,7 +448,7 @@
 section {* Substitution Operation on equations *}
 
 text {* 
-  Suppose and equation @{text "X = xrhs"}, @{text "subst_op"} substitutes 
+  Suppose and equation @{text "X = xrhs"}, @{text "Subst"} substitutes 
   all occurences of @{text "X"} in @{text "rhs"} by @{text "xrhs"}.
 *}
 
@@ -476,7 +476,7 @@
   *}
 
 definition
-  "remove_op ES Y yrhs \<equiv> 
+  "Remove ES Y yrhs \<equiv> 
       Subst_all  (ES - {(Y, yrhs)}) Y (Arden Y yrhs)"
 
 text {*
@@ -486,7 +486,7 @@
 
 definition 
   "iter X ES \<equiv> (let (Y, yrhs) = SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> (X \<noteq> Y)
-                in remove_op ES Y yrhs)"
+                in Remove ES Y yrhs)"
 
 text {*
   The following term @{text "reduce X ES"} repeatedly removes characteriztion equations
@@ -911,7 +911,6 @@
 by (auto simp:classes_of_def)
 
 lemma Subst_all_keeps_self_contained:
-  fixes Y
   assumes sc: "self_contained (ES \<union> {(Y, yrhs)})" (is "self_contained ?A")
   shows "self_contained (Subst_all ES Y (Arden Y yrhs))" 
                                                    (is "self_contained ?B")
@@ -1046,7 +1045,7 @@
     using not_T X_in_ES by (drule_tac card_noteq_1_has_more, auto)
   let ?ES' = "iter X ES"
   show ?thesis
-  proof(unfold iter_def remove_op_def, rule someI2 [where a = "(Y, yrhs)"], clarsimp)
+  proof(unfold iter_def Remove_def, rule someI2 [where a = "(Y, yrhs)"], clarsimp)
     from X_in_ES Y_in_ES and not_eq and Inv_ES
     show "(Y, yrhs) \<in> ES \<and> X \<noteq> Y"
       by (auto simp: invariant_def distinct_equas_def)