src/HOLCF/IOA/meta_theory/CompoTraces.ML
changeset 4813 14cea5b1d12f
parent 4678 78715f589655
child 4833 2e53109d4bc8
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Tue Apr 21 10:49:15 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Tue Apr 21 17:20:28 1998 +0200
@@ -729,9 +729,7 @@
 by (Asm_simp_tac 1);
 (* first side: mksch = UU *)
 by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPUU,
-                                           (finiteR_mksch RS mp COMP rev_contrapos),
-                                            ForallBnAmksch],
-                           simpset())) 1);
+        (finiteR_mksch RS mp COMP rev_contrapos),ForallBnAmksch],simpset())) 1);
 (* schA = UU *)
 by (eres_inst_tac [("A","A")] LastActExtimplUU 1);
 by (Asm_simp_tac 1);