changeset 42814 | 5af15f1e2ef6 |
parent 42786 | 06a38b936342 |
child 43596 | 78211f66cf8d |
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Sun May 15 17:06:35 2011 +0200 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Sun May 15 17:45:53 2011 +0200 @@ -803,7 +803,7 @@ method_setup split_idle = {* Method.sections (Simplifier.simp_modifiers @ Splitter.split_modifiers) >> (K (SIMPLE_METHOD' o split_idle_tac)) -*} "" +*} (* ---------------------------------------------------------------------- Combine steps 1.2 and 1.4 to prove that the implementation satisfies