summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Tue, 14 Nov 2017 16:17:08 +0100 | |

changeset 67073 | 74bd55f1206d |

parent 67070 | 85e6c1ff5be3 (current diff) |

parent 67072 | b5c1f0c76d35 (diff) |

child 67074 | 5da20135f560 |

merged

--- a/src/HOL/IMP/Big_Step.thy Tue Nov 14 13:56:38 2017 +0100 +++ b/src/HOL/IMP/Big_Step.thy Tue Nov 14 16:17:08 2017 +0100 @@ -206,13 +206,11 @@ thus ?thesis using `\<not>bval b s` by blast next case IfTrue - with `(?iw, s) \<Rightarrow> t` have "(c;; ?w, s) \<Rightarrow> t" by auto -- "and for this, only the Seq-rule is applicable:" - then obtain s' where + from `(c;; ?w, s) \<Rightarrow> t` obtain s' where "(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> 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