equal
deleted
inserted
replaced
119 (e \<tturnstile> ts : Ts \<and> e \<turnstile> t : T)" |
119 (e \<tturnstile> ts : Ts \<and> e \<turnstile> t : T)" |
120 apply (induct ts) |
120 apply (induct ts) |
121 apply (case_tac Ts) |
121 apply (case_tac Ts) |
122 apply simp+ |
122 apply simp+ |
123 apply (case_tac Ts) |
123 apply (case_tac Ts) |
124 apply (case_tac "list @ [t]") |
124 apply (case_tac "ts @ [t]") |
125 apply simp+ |
125 apply simp+ |
126 done |
126 done |
127 |
127 |
128 lemma rev_exhaust2 [case_names Nil snoc, extraction_expand]: |
128 lemma rev_exhaust2 [case_names Nil snoc, extraction_expand]: |
129 "(xs = [] \<Longrightarrow> P) \<Longrightarrow> (\<And>ys y. xs = ys @ [y] \<Longrightarrow> P) \<Longrightarrow> P" |
129 "(xs = [] \<Longrightarrow> P) \<Longrightarrow> (\<And>ys y. xs = ys @ [y] \<Longrightarrow> P) \<Longrightarrow> P" |
183 apply (case_tac Ts) |
183 apply (case_tac Ts) |
184 apply simp |
184 apply simp |
185 apply simp |
185 apply simp |
186 apply (erule_tac x = "t \<degree> a" in allE) |
186 apply (erule_tac x = "t \<degree> a" in allE) |
187 apply (erule_tac x = T in allE) |
187 apply (erule_tac x = T in allE) |
188 apply (erule_tac x = lista in allE) |
188 apply (erule_tac x = list in allE) |
189 apply (erule impE) |
189 apply (erule impE) |
190 apply (erule conjE) |
190 apply (erule conjE) |
191 apply (erule typing.App) |
191 apply (erule typing.App) |
192 apply assumption |
192 apply assumption |
193 apply blast |
193 apply blast |