--- a/src/HOL/IMP/Star.thy Tue Oct 25 12:00:52 2011 +0200
+++ b/src/HOL/IMP/Star.thy Tue Oct 25 15:59:15 2011 +0200
@@ -7,6 +7,8 @@
refl: "star r x x" |
step: "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
+hide_fact (open) refl step --"names too generic"
+
lemma star_trans:
"star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
proof(induction rule: star.induct)
@@ -19,8 +21,8 @@
declare star.refl[simp,intro]
-lemma step1[simp, intro]: "r x y \<Longrightarrow> star r x y"
-by(metis refl step)
+lemma star_step1[simp, intro]: "r x y \<Longrightarrow> star r x y"
+by(metis star.refl star.step)
code_pred star .