changeset 45606 | b1e1508643b1 |
parent 42151 | 4da4fc77664b |
child 51703 | f2e92fc0c8aa |
--- a/src/HOL/HOLCF/IOA/meta_theory/Traces.thy Sun Nov 20 21:05:23 2011 +0100 +++ b/src/HOL/HOLCF/IOA/meta_theory/Traces.thy Sun Nov 20 21:07:06 2011 +0100 @@ -402,7 +402,7 @@ done lemmas exec_prefixclosed = - conjI [THEN execfrag_prefixclosed [THEN spec, THEN spec, THEN mp], standard] + conjI [THEN execfrag_prefixclosed [THEN spec, THEN spec, THEN mp]] (* second prefix notion for Finite x *)