# HG changeset patch
# User paulson
# Date 882874186 -3600
# Node ID 803d1e302af1f30fb1d58bb6ffc15afc35867a8f
# Parent  cfa3bd184bc1c88d00ef48631fba8f496b9ea831
Decremented subscript because of change to iffD1

diff -r cfa3bd184bc1 -r 803d1e302af1 src/HOL/Integ/Integ.ML
--- a/src/HOL/Integ/Integ.ML	Tue Dec 23 11:47:13 1997 +0100
+++ b/src/HOL/Integ/Integ.ML	Tue Dec 23 11:49:46 1997 +0100
@@ -22,7 +22,7 @@
 val eqa::eqb::prems = goal Arith.thy 
     "[| (x1::nat) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] ==> \
 \       x1 + y3 = x3 + y1";
-by (res_inst_tac [("k2","x2")] (add_left_cancel RS iffD1) 1);
+by (res_inst_tac [("k1","x2")] (add_left_cancel RS iffD1) 1);
 by (rtac (add_left_commute RS trans) 1);
 by (stac eqb 1);
 by (rtac (add_left_commute RS trans) 1);
diff -r cfa3bd184bc1 -r 803d1e302af1 src/HOLCF/IOA/meta_theory/Automata.ML
--- a/src/HOLCF/IOA/meta_theory/Automata.ML	Tue Dec 23 11:47:13 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Automata.ML	Tue Dec 23 11:49:46 1997 +0100
@@ -205,7 +205,7 @@
 by (eres_inst_tac [("x","a")] allE 1);
 by (eres_inst_tac [("x","a")] allE 1);
 by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
-by (forw_inst_tac [("A2","A")] (compat_commute RS iffD1) 1);
+by (forw_inst_tac [("A1","A")] (compat_commute RS iffD1) 1);
 by (dtac inpAAactB_is_inpBoroutB 1);
 back();
 by (assume_tac 1);
diff -r cfa3bd184bc1 -r 803d1e302af1 src/HOLCF/IOA/meta_theory/CompoTraces.ML
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Tue Dec 23 11:47:13 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Tue Dec 23 11:49:46 1997 +0100
@@ -289,7 +289,7 @@
 \                   Forall (%x. x:act B & x~:act A) y1 & \
 \                   Finite y1 & y = (y1 @@ y2) & \
 \                   Filter (%a. a:ext B)`y1 = bs)";
-by (forw_inst_tac [("A2","A")] (compat_commute RS iffD1) 1);
+by (forw_inst_tac [("A1","A")] (compat_commute RS iffD1) 1);
 by (etac Seq_Finite_ind  1);
 by (REPEAT (rtac allI 1));
 by (rtac impI 1);
@@ -344,7 +344,7 @@
 \                   Forall (%x. x:act A & x~:act B) x1 & \
 \                   Finite x1 & x = (x1 @@ x2) & \
 \                   Filter (%a. a:ext A)`x1 = as)";
-by (forw_inst_tac [("A2","A")] (compat_commute RS iffD1) 1);
+by (forw_inst_tac [("A1","A")] (compat_commute RS iffD1) 1);
 by (etac Seq_Finite_ind  1);
 by (REPEAT (rtac allI 1));
 by (rtac impI 1);
diff -r cfa3bd184bc1 -r 803d1e302af1 src/HOLCF/IOA/meta_theory/Compositionality.ML
--- a/src/HOLCF/IOA/meta_theory/Compositionality.ML	Tue Dec 23 11:47:13 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML	Tue Dec 23 11:49:46 1997 +0100
@@ -59,8 +59,8 @@
 \        ==> (A1 || B1) =<| (A2 || B2)";
 
 by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def]) 1);
-by (forw_inst_tac [("A2","A1")] (compat_commute RS iffD1) 1);
-by (forw_inst_tac [("A2","A2")] (compat_commute RS iffD1) 1);
+by (forw_inst_tac [("A1","A1")] (compat_commute RS iffD1) 1);
+by (forw_inst_tac [("A1","A2")] (compat_commute RS iffD1) 1);
 by (asm_full_simp_tac (simpset() addsimps [ioa_implements_def,
           inputs_of_par,outputs_of_par,externals_of_par]) 1);
 by (safe_tac set_cs);