1.1 --- a/src/HOL/Induct/Common_Patterns.thy	Tue Sep 03 13:09:15 2013 +0200
     1.2 +++ b/src/HOL/Induct/Common_Patterns.thy	Tue Sep 03 18:21:43 2013 +0200
     1.3 @@ -388,19 +388,18 @@
     1.4    refl: "star r x x"
     1.5  | step: "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
     1.6  
     1.7 -text{* Underscores are replaced by the default name hyps: *}
     1.8 +text {* Underscores are replaced by the default name hyps: *}
     1.9  
    1.10 -lemmas star_induct = star.induct[case_names base step[r _ IH]]
    1.11 +lemmas star_induct = star.induct [case_names base step[r _ IH]]
    1.12  
    1.13  lemma "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
    1.14 -proof(induct rule: star_induct)
    1.15 -print_cases
    1.16 -  case base thus ?case .
    1.17 +proof (induct rule: star_induct) print_cases
    1.18 +  case base
    1.19 +  then show ?case .
    1.20  next
    1.21 -  case (step a b c)
    1.22 -  from step.prems have "star r b z" by(rule step.IH)
    1.23 -  from step.r this show ?case by(rule star.step)
    1.24 +  case (step a b c) print_facts
    1.25 +  from step.prems have "star r b z" by (rule step.IH)
    1.26 +  with step.r show ?case by (rule star.step)
    1.27  qed
    1.28  
    1.29 -
    1.30  end
    1.31 \ No newline at end of file