| changeset 50054 | 6da283e4497b |
| parent 45265 | 521508e85c0d |
| child 67406 | 23307fd33906 |
--- a/src/HOL/IMP/Star.thy Mon Nov 12 14:46:42 2012 +0100 +++ b/src/HOL/IMP/Star.thy Mon Nov 12 18:42:49 2012 +0100 @@ -17,7 +17,8 @@ case step thus ?case by (metis star.step) qed -lemmas star_induct = star.induct[of "r:: 'a*'b \<Rightarrow> 'a*'b \<Rightarrow> bool", split_format(complete)] +lemmas star_induct = + star.induct[of "r:: 'a*'b \<Rightarrow> 'a*'b \<Rightarrow> bool", split_format(complete)] declare star.refl[simp,intro]