equal
deleted
inserted
replaced
1119 fun lambda_prs_conv quot = |
1119 fun lambda_prs_conv quot = |
1120 More_Conv.top_conv (lambda_prs_simple_conv quot) |
1120 More_Conv.top_conv (lambda_prs_simple_conv quot) |
1121 *} |
1121 *} |
1122 |
1122 |
1123 ML {* |
1123 ML {* |
1124 fun lambda_prs_tac quot ctxt = CONVERSION |
1124 fun lambda_prs_tac quot ctxt = CONVERSION (lambda_prs_conv quot ctxt) |
1125 (Conv.params_conv ~1 (fn ctxt => |
|
1126 (Conv.prems_conv ~1 (lambda_prs_conv quot ctxt) then_conv |
|
1127 Conv.concl_conv ~1 (lambda_prs_conv quot ctxt))) ctxt) |
|
1128 *} |
1125 *} |
1129 |
1126 |
1130 (* |
1127 (* |
1131 Cleaning the theorem consists of 6 kinds of rewrites. |
1128 Cleaning the theorem consists of 6 kinds of rewrites. |
1132 The first two need to be done before fun_map is unfolded |
1129 The first two need to be done before fun_map is unfolded |