# HG changeset patch
# User paulson
# Date 997109020 -7200
# Node ID 1064effe37f6bcea84da4d411cf905e0c478024b
# Parent  d64ccdeaf9ae1bd92d1b6412cd2ee3b23a988a73
Converted 1 to 1'

diff -r d64ccdeaf9ae -r 1064effe37f6 src/HOL/UNITY/Extend.ML
--- a/src/HOL/UNITY/Extend.ML	Mon Aug 06 15:54:29 2001 +0200
+++ b/src/HOL/UNITY/Extend.ML	Mon Aug 06 16:43:40 2001 +0200
@@ -753,14 +753,11 @@
 by (auto_tac (claset(), simpset() addsimps [ok_def]));  
 qed "ok_extend_iff";
 
-Unify.search_bound := 40;
-Unify.trace_bound  := 40;
-
-Goal "OK I (%i. extend h (F i)) = (OK I F)";
-by (auto_tac (claset(), simpset() addsimps [OK_def]));  
+Goalw [OK_def] "OK I (%i. extend h (F i)) = (OK I F)";
+by Safe_tac;
 by (dres_inst_tac [("x","i")] bspec 1); 
-by (dres_inst_tac [("x","j")] bspec 2); 
-by Auto_tac;  
+by (dres_inst_tac [("x","j")] bspec 2);  
+by (REPEAT (Force_tac 1));
 qed "OK_extend_iff";
 
 Goal "F : X guarantees Y ==> \
diff -r d64ccdeaf9ae -r 1064effe37f6 src/HOL/UNITY/Lift_prog.ML
--- a/src/HOL/UNITY/Lift_prog.ML	Mon Aug 06 15:54:29 2001 +0200
+++ b/src/HOL/UNITY/Lift_prog.ML	Mon Aug 06 16:43:40 2001 +0200
@@ -309,7 +309,7 @@
 Goal "(insert_map j t f)(i := s) = \
 \     (if i=j then insert_map i s f \
 \      else if i<j then insert_map j t (f(i:=s)) \
-\      else insert_map j t (f(i-1:=s)))";
+\      else insert_map j t (f(i-1' := s)))";
 by (rtac ext 1);
 by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
 by (ALLGOALS arith_tac);
@@ -341,7 +341,7 @@
 by (dtac subsetD 1);
 by (Blast_tac 1);
 by Auto_tac;
-ren "s f uu s' f' uu'" 1;
+by (rename_tac "s f uu s' f' uu'" 1);
 by (subgoal_tac "f'=f & uu'=uu" 1);
 by (force_tac (claset() addSDs [preserves_imp_eq], simpset()) 2);
 by Auto_tac;
diff -r d64ccdeaf9ae -r 1064effe37f6 src/HOL/UNITY/Simple/Network.ML
--- a/src/HOL/UNITY/Simple/Network.ML	Mon Aug 06 15:54:29 2001 +0200
+++ b/src/HOL/UNITY/Simple/Network.ML	Mon Aug 06 16:43:40 2001 +0200
@@ -14,11 +14,11 @@
 \      !! m. F : stable {s. s(Aproc,Rcvd) <= s(Bproc,Sent)};  \
 \      !! m proc. F : stable {s. m <= s(proc,Sent)};  \
 \      !! n proc. F : stable {s. n <= s(proc,Rcvd)};  \
-\      !! m proc. F : {s. s(proc,Idle) = 1 & s(proc,Rcvd) = m} co \
-\                                 {s. s(proc,Rcvd) = m --> s(proc,Idle) = 1}; \
-\      !! n proc. F : {s. s(proc,Idle) = 1 & s(proc,Sent) = n} co \
+\      !! m proc. F : {s. s(proc,Idle) = 1' & s(proc,Rcvd) = m} co \
+\                                 {s. s(proc,Rcvd) = m --> s(proc,Idle) = 1'}; \
+\      !! n proc. F : {s. s(proc,Idle) = 1' & s(proc,Sent) = n} co \
 \                                 {s. s(proc,Sent) = n} \
-\   |] ==> F : stable {s. s(Aproc,Idle) = 1 & s(Bproc,Idle) = 1 & \
+\   |] ==> F : stable {s. s(Aproc,Idle) = 1' & s(Bproc,Idle) = 1' & \
 \                         s(Aproc,Sent) = s(Bproc,Rcvd) & \
 \                         s(Bproc,Sent) = s(Aproc,Rcvd) & \
 \                         s(Aproc,Rcvd) = m & s(Bproc,Rcvd) = n}";
diff -r d64ccdeaf9ae -r 1064effe37f6 src/HOL/UNITY/Simple/Reachability.ML
--- a/src/HOL/UNITY/Simple/Reachability.ML	Mon Aug 06 15:54:29 2001 +0200
+++ b/src/HOL/UNITY/Simple/Reachability.ML	Mon Aug 06 16:43:40 2001 +0200
@@ -162,7 +162,7 @@
 
 
 Goalw [nmsg_gte_def, nmsg_lte_def,nmsg_gt_def, nmsg_eq_def]
-     "((nmsg_gte 0 (v,w) Int nmsg_lte 1 (v,w)) Int (- nmsg_gt 0 (v,w) Un A)) \
+     "((nmsg_gte 0 (v,w) Int nmsg_lte 1' (v,w)) Int (- nmsg_gt 0 (v,w) Un A)) \
 \     <= A Un nmsg_eq 0 (v,w)";
 by Auto_tac;
 qed "lemma4";
@@ -170,7 +170,7 @@
 
 Goalw [nmsg_gte_def,nmsg_lte_def,nmsg_gt_def, nmsg_eq_def]
      "reachable v Int nmsg_eq 0 (v,w) = \
-\     ((nmsg_gte 0 (v,w) Int nmsg_lte 1 (v,w)) Int \
+\     ((nmsg_gte 0 (v,w) Int nmsg_lte 1' (v,w)) Int \
 \      (reachable v Int nmsg_lte 0 (v,w)))";
 by Auto_tac;
 qed "lemma5";
diff -r d64ccdeaf9ae -r 1064effe37f6 src/HOL/UNITY/Simple/Reachability.thy
--- a/src/HOL/UNITY/Simple/Reachability.thy	Mon Aug 06 15:54:29 2001 +0200
+++ b/src/HOL/UNITY/Simple/Reachability.thy	Mon Aug 06 16:43:40 2001 +0200
@@ -60,7 +60,7 @@
 
     MA4  "[|(v,w) : E|] ==> F : Always (-(reachable v) Un (nmsg_gt 0 (v,w)) Un (reachable w))"
 
-    MA5  "[|v:V;w:V|] ==> F : Always (nmsg_gte 0 (v,w) Int nmsg_lte 1 (v,w))"
+    MA5  "[|v:V;w:V|] ==> F : Always (nmsg_gte 0 (v,w) Int nmsg_lte 1' (v,w))"
 
     MA6  "[|v:V|] ==> F : Stable (reachable v)"
 
diff -r d64ccdeaf9ae -r 1064effe37f6 src/HOL/UNITY/Union.ML
--- a/src/HOL/UNITY/Union.ML	Mon Aug 06 15:54:29 2001 +0200
+++ b/src/HOL/UNITY/Union.ML	Mon Aug 06 16:43:40 2001 +0200
@@ -352,7 +352,7 @@
 
 bind_thm ("ok_sym", ok_commute RS iffD1);
 
-Goal "OK {(0,F),(1,G),(2,H)} snd = (F ok G & (F Join G) ok H)";
+Goal "OK {(#0::int,F),(#1,G),(#2,H)} snd = (F ok G & (F Join G) ok H)";
 by (asm_full_simp_tac
     (simpset() addsimps [Ball_def, conj_disj_distribR, ok_def, Join_def, 
                    OK_def, insert_absorb, all_conj_distrib, eq_commute]) 1);