| changeset 10458 | df4e182c0fcd |
| parent 10007 | 64bf7da1994a |
| child 11809 | c9ffdd63dd93 |
| 10457:dd669bda2b0c | 10458:df4e182c0fcd |
|---|---|
81 proof (induct (open) ?P t rule: term_induct') |
81 proof (induct (open) ?P t rule: term_induct') |
82 case Var |
82 case Var |
83 show "?P (Var a)" by (simp add: o_def) |
83 show "?P (Var a)" by (simp add: o_def) |
84 next |
84 next |
85 case App |
85 case App |
86 have "?this --> ?P (App b ts)" |
86 show "?P (App b ts)" by (insert App, induct ts) simp_all |
87 by (induct ts) simp_all |
|
88 thus "..." .. |
|
89 qed |
87 qed |
90 |
88 |
91 end |
89 end |