diff -r e2ab4147b244 -r fa37ee54644c src/HOL/Hoare_Parallel/RG_Examples.thy --- a/src/HOL/Hoare_Parallel/RG_Examples.thy Tue Dec 03 22:46:24 2024 +0100 +++ b/src/HOL/Hoare_Parallel/RG_Examples.thy Fri Dec 06 13:33:25 2024 +0100 @@ -117,11 +117,11 @@ apply simp apply clarify apply simp - apply(subgoal_tac "xa=0") + apply(subgoal_tac "x=0") apply simp apply arith apply clarify - apply(case_tac xaa, simp, simp) + apply(case_tac xa, simp, simp) apply clarify apply simp apply(erule_tac x=0 in all_dupE)