--- a/src/HOL/Library/While_Combinator.thy Sun Apr 24 21:31:14 2016 +0200
+++ b/src/HOL/Library/While_Combinator.thy Mon Apr 25 16:09:26 2016 +0200
@@ -60,12 +60,12 @@
by(metis while_option_stop2)
theorem while_option_rule:
-assumes step: "!!s. P s ==> b s ==> P (c s)"
-and result: "while_option b c s = Some t"
-and init: "P s"
-shows "P t"
+ assumes step: "!!s. P s ==> b s ==> P (c s)"
+ and result: "while_option b c s = Some t"
+ and init: "P s"
+ shows "P t"
proof -
- def k == "LEAST k. ~ b ((c ^^ k) s)"
+ define k where "k = (LEAST k. ~ b ((c ^^ k) s))"
from assms have t: "t = (c ^^ k) s"
by (simp add: while_option_def k_def split: if_splits)
have 1: "ALL i<k. b ((c ^^ i) s)"