equal
deleted
inserted
replaced
109 apply (tactic {* ALLGOALS (REPEAT o thin_tac @{context} "ehoare ?x ?y") *}) |
109 apply (tactic {* ALLGOALS (REPEAT o thin_tac @{context} "ehoare ?x ?y") *}) |
110 apply (simp_all only: cnvalid1_eq cenvalid_def2) |
110 apply (simp_all only: cnvalid1_eq cenvalid_def2) |
111 apply fast |
111 apply fast |
112 apply fast |
112 apply fast |
113 apply fast |
113 apply fast |
114 apply (clarify,tactic "smp_tac 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+) |
114 apply (clarify,tactic "smp_tac @{context} 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+) |
115 apply fast |
115 apply fast |
116 apply fast |
116 apply fast |
117 apply fast |
117 apply fast |
118 apply fast |
118 apply fast |
119 apply fast |
119 apply fast |