equal
deleted
inserted
replaced
1054 show "\<And> B' A'. \<lbrakk>Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'; B \<subseteq> B'\<rbrakk> |
1054 show "\<And> B' A'. \<lbrakk>Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'; B \<subseteq> B'\<rbrakk> |
1055 \<Longrightarrow> (nrm A \<subseteq> nrm A') \<and> (\<forall> l. (brk A l \<subseteq> brk A' l))" |
1055 \<Longrightarrow> (nrm A \<subseteq> nrm A') \<and> (\<forall> l. (brk A l \<subseteq> brk A' l))" |
1056 (is "PROP ?Hyp Env B t A") |
1056 (is "PROP ?Hyp Env B t A") |
1057 proof (induct) |
1057 proof (induct) |
1058 case Skip |
1058 case Skip |
1059 from Skip.prems Skip.hyps |
1059 then show ?case by cases simp |
1060 show ?case by cases simp |
|
1061 next |
1060 next |
1062 case Expr |
1061 case Expr |
1063 from Expr.prems Expr.hyps |
1062 from Expr.prems Expr.hyps |
1064 show ?case by cases simp |
1063 show ?case by cases simp |
1065 next |
1064 next |