| changeset 58219 | 61b852f90161 |
| parent 54703 | 499f92dc6e45 |
| child 58249 | 180f1b3508ed |
| 58218:a92acec845a7 | 58219:61b852f90161 |
|---|---|
581 shows "(\<exists>t'. t \<longrightarrow>cbv t') \<or> (val t)" |
581 shows "(\<exists>t'. t \<longrightarrow>cbv t') \<or> (val t)" |
582 using a |
582 using a |
583 by (induct \<Gamma>\<equiv>"[]::tctx" t T) |
583 by (induct \<Gamma>\<equiv>"[]::tctx" t T) |
584 (auto dest!: canonical_tINT intro!: cbv.intros gr0I) |
584 (auto dest!: canonical_tINT intro!: cbv.intros gr0I) |
585 |
585 |
586 end |
586 end |
587 |
587 |
588 |
|
589 |
|
590 |
|
591 |
|
592 |
|
593 |
|
594 |
|
595 |
|
596 |