# HG changeset patch
# User wenzelm
# Date 1378225303 -7200
# Node ID 74920496ab718ed5c6f144c9306d46427ebc7fc1
# Parent  07990ba8c0ead3ad91d23e2dbacf1d67dfcad9cc
minor tuning;

diff -r 07990ba8c0ea -r 74920496ab71 src/HOL/Induct/Common_Patterns.thy
--- a/src/HOL/Induct/Common_Patterns.thy	Tue Sep 03 13:09:15 2013 +0200
+++ b/src/HOL/Induct/Common_Patterns.thy	Tue Sep 03 18:21:43 2013 +0200
@@ -388,19 +388,18 @@
   refl: "star r x x"
 | step: "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
 
-text{* Underscores are replaced by the default name hyps: *}
+text {* Underscores are replaced by the default name hyps: *}
 
-lemmas star_induct = star.induct[case_names base step[r _ IH]]
+lemmas star_induct = star.induct [case_names base step[r _ IH]]
 
 lemma "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
-proof(induct rule: star_induct)
-print_cases
-  case base thus ?case .
+proof (induct rule: star_induct) print_cases
+  case base
+  then show ?case .
 next
-  case (step a b c)
-  from step.prems have "star r b z" by(rule step.IH)
-  from step.r this show ?case by(rule star.step)
+  case (step a b c) print_facts
+  from step.prems have "star r b z" by (rule step.IH)
+  with step.r show ?case by (rule star.step)
 qed
 
-
 end
\ No newline at end of file