# HG changeset patch
# User nipkow
# Date 1510661533 -3600
# Node ID a462583f0a37dde46b4364e9e10d93f1e29f264d
# Parent c1b87d15774a0527c7831f543047320e30b7c89c
tuned
diff -r c1b87d15774a -r a462583f0a37 src/HOL/IMP/Big_Step.thy
--- a/src/HOL/IMP/Big_Step.thy Fri Nov 10 22:05:30 2017 +0100
+++ b/src/HOL/IMP/Big_Step.thy Tue Nov 14 13:12:13 2017 +0100
@@ -206,13 +206,11 @@
thus ?thesis using `\bval b s` by blast
next
case IfTrue
- with `(?iw, s) \ t` have "(c;; ?w, s) \ t" by auto
-- "and for this, only the Seq-rule is applicable:"
- then obtain s' where
+ from `(c;; ?w, s) \ t` obtain s' where
"(c, s) \ s'" and "(?w, s') \ t" by auto
- -- "with this information, we can build a derivation tree for the @{text WHILE}"
- with `bval b s`
- show ?thesis by (rule WhileTrue)
+ -- "with this information, we can build a derivation tree for @{text WHILE}"
+ with `bval b s` show ?thesis by (rule WhileTrue)
qed
qed
ultimately