equal
deleted
inserted
replaced
585 |
585 |
586 |
586 |
587 ML {* prop_of t_a *} |
587 ML {* prop_of t_a *} |
588 ML {* term_of glac *} |
588 ML {* term_of glac *} |
589 ML {* val (tta, ttb) = (my_reg2 @{context} (prop_of t_a) (term_of glac)) *} |
589 ML {* val (tta, ttb) = (my_reg2 @{context} (prop_of t_a) (term_of glac)) *} |
|
590 |
|
591 (* Does not work. *) |
|
592 (* ML {* val ttar = REGULARIZE_trm @{context} (prop_of t_a) (term_of glac) *} *) |
|
593 |
590 ML {* val tt = Syntax.check_term @{context} tta *} |
594 ML {* val tt = Syntax.check_term @{context} tta *} |
591 |
595 |
592 prove t_r: {* Logic.mk_implies |
596 prove t_r: {* Logic.mk_implies |
593 ((prop_of t_a), tt) *} |
597 ((prop_of t_a), tt) *} |
594 ML_prf {* fun tac ctxt = FIRST' [ |
598 ML_prf {* fun tac ctxt = FIRST' [ |