# HG changeset patch
# User mueller
# Date 873796532 -7200
# Node ID 4be700757406a66fafc178e9f41755253a1dd939
# Parent  1ea4a45b9412e8902f09cf7f4c5856957f042e85
adm_tac extended

diff -r 1ea4a45b9412 -r 4be700757406 src/HOLCF/IOA/meta_theory/Automata.ML
--- a/src/HOLCF/IOA/meta_theory/Automata.ML	Tue Sep 09 11:14:20 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.ML	Tue Sep 09 11:15:32 1997 +0200
@@ -296,7 +296,7 @@
 \         trans_of(restrict ioa acts) = trans_of(ioa) & \
 \         reachable (restrict ioa acts) s = reachable ioa s & \
 \         act (restrict A acts) = act A";
-by (simp_tac (!simpset addsimps [cancel_restrict_a,cancel_restrict_b,acts_restrict]) 1);
+  by (simp_tac (!simpset addsimps [cancel_restrict_a,cancel_restrict_b,acts_restrict]) 1);
 qed"cancel_restrict";
 
 (* ---------------------------------------------------------------------------------- *)
diff -r 1ea4a45b9412 -r 4be700757406 src/HOLCF/IOA/meta_theory/Sequence.ML
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Tue Sep 09 11:14:20 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Tue Sep 09 11:15:32 1997 +0200
@@ -7,9 +7,6 @@
 
 *)
 
-(* re-add extended adm_tactic, as it has been lost during theory merge *) 
-simpset := !simpset addSolver(fn thms =>
-            (adm_tac (cut_facts_tac thms THEN' cont_tacRs)));
 
 Addsimps [andalso_and,andalso_or];