equal
deleted
inserted
replaced
601 (term_of glac) |
601 (term_of glac) |
602 |> Syntax.string_of_term @{context} |
602 |> Syntax.string_of_term @{context} |
603 |> writeln |
603 |> writeln |
604 *} |
604 *} |
605 |
605 |
606 ML {* val ttar = REGULARIZE_trm @{context} (prop_of t_a) (term_of glac) *} |
606 ML {* val tta = REGULARIZE_trm @{context} (prop_of t_a) (term_of glac) *} |
607 |
607 |
608 ML {* val tt = Syntax.check_term @{context} tta *} |
608 ML {* val tt = Syntax.check_term @{context} tta *} |
609 ML {* val ttr = Syntax.check_term @{context} ttar *} |
|
610 |
609 |
611 |
610 |
612 |
611 |
613 prove t_r: {* Logic.mk_implies |
612 prove t_r: {* Logic.mk_implies |
614 ((prop_of t_a), tt) *} |
613 ((prop_of t_a), tt) *} |