equal
deleted
inserted
replaced
465 [N (Refl, []), N (Refl, [])])])])); |
465 [N (Refl, []), N (Refl, [])])])])); |
466 |
466 |
467 reconstruct_proof @{context} proof24 |
467 reconstruct_proof @{context} proof24 |
468 \<close> |
468 \<close> |
469 |
469 |
|
470 ML \<open> |
|
471 val proof25 = |
|
472 ((@{term "let vr0 = vr1 in let vr1 = vr2 in vr0 + vr1 + vr2 :: nat"}, |
|
473 @{term "vr1 + vr2 + vr2 :: nat"}), |
|
474 N (Trans @{term "let vr1a = vr2 in vr1 + vr1a + vr2 :: nat"}, |
|
475 [N (Let [@{term "vr1 :: nat"}], [N (Refl, []), N (Refl, [])]), |
|
476 N (Let [@{term "vr2 :: nat"}], [N (Refl, []), N (Refl, [])])])); |
|
477 |
|
478 reconstruct_proof @{context} proof18 |
|
479 \<close> |
|
480 |
470 end |
481 end |