author | nipkow |

Tue Nov 14 13:12:13 2017 +0100 (9 months ago) | |

changeset 67071 | a462583f0a37 |

parent 67040 | c1b87d15774a |

child 67072 | b5c1f0c76d35 |

tuned

1.1 --- a/src/HOL/IMP/Big_Step.thy Fri Nov 10 22:05:30 2017 +0100 1.2 +++ b/src/HOL/IMP/Big_Step.thy Tue Nov 14 13:12:13 2017 +0100 1.3 @@ -206,13 +206,11 @@ 1.4 thus ?thesis using `\<not>bval b s` by blast 1.5 next 1.6 case IfTrue 1.7 - with `(?iw, s) \<Rightarrow> t` have "(c;; ?w, s) \<Rightarrow> t" by auto 1.8 -- "and for this, only the Seq-rule is applicable:" 1.9 - then obtain s' where 1.10 + from `(c;; ?w, s) \<Rightarrow> t` obtain s' where 1.11 "(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto 1.12 - -- "with this information, we can build a derivation tree for the @{text WHILE}" 1.13 - with `bval b s` 1.14 - show ?thesis by (rule WhileTrue) 1.15 + -- "with this information, we can build a derivation tree for @{text WHILE}" 1.16 + with `bval b s` show ?thesis by (rule WhileTrue) 1.17 qed 1.18 qed 1.19 ultimately