changeset 44045 | 2814ff2a6e3e |
parent 41778 | 5f79a9e42507 |
child 44890 | 22f665a2e91c |
--- a/src/HOL/Bali/DefiniteAssignment.thy Sun Jul 31 11:13:38 2011 -0700 +++ b/src/HOL/Bali/DefiniteAssignment.thy Mon Aug 01 12:08:53 2011 +0200 @@ -1056,8 +1056,7 @@ (is "PROP ?Hyp Env B t A") proof (induct) case Skip - from Skip.prems Skip.hyps - show ?case by cases simp + then show ?case by cases simp next case Expr from Expr.prems Expr.hyps