equal
deleted
inserted
replaced
310 let |
310 let |
311 val t = (case to of NONE => HOLogic.dest_Trueprop goal | SOME x => x) |
311 val t = (case to of NONE => HOLogic.dest_Trueprop goal | SOME x => x) |
312 val th = genreflect ctxt conv corr_thms raw_eqs t RS ssubst |
312 val th = genreflect ctxt conv corr_thms raw_eqs t RS ssubst |
313 in rtac th i THEN TRY (rtac TrueI i) end); (* FIXME THEN_ALL_NEW !? *) |
313 in rtac th i THEN TRY (rtac TrueI i) end); (* FIXME THEN_ALL_NEW !? *) |
314 |
314 |
315 fun reflection_tac ctxt = gen_reflection_tac ctxt (Codegen.evaluation_conv ctxt); |
315 fun reflection_tac ctxt = gen_reflection_tac ctxt |
316 (*FIXME why Codegen.evaluation_conv? very specific...*) |
316 (Code_Evaluation.dynamic_conv (Proof_Context.theory_of ctxt)); |
|
317 (*FIXME why Code_Evaluation.dynamic_conv? very specific...*) |
317 |
318 |
318 end |
319 end |