equal
deleted
inserted
replaced
73 fun current_tac thy = CONVERSION (current_conv thy) THEN' conclude_tac thy NONE; |
73 fun current_tac thy = CONVERSION (current_conv thy) THEN' conclude_tac thy NONE; |
74 |
74 |
75 fun current_value thy = snd o Logic.dest_equals o Thm.prop_of o current_conv thy o Thm.cterm_of thy; |
75 fun current_value thy = snd o Logic.dest_equals o Thm.prop_of o current_conv thy o Thm.cterm_of thy; |
76 |
76 |
77 val setup = Method.setup (Binding.name "code_simp") |
77 val setup = Method.setup (Binding.name "code_simp") |
78 (Scan.succeed (SIMPLE_METHOD' o current_tac o ProofContext.theory_of)) |
78 (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo current_tac o ProofContext.theory_of))) |
79 "simplification with code equations" |
79 "simplification with code equations" |
80 #> Value.add_evaluator ("simp", current_value o ProofContext.theory_of); |
80 #> Value.add_evaluator ("simp", current_value o ProofContext.theory_of); |
81 |
81 |
82 |
82 |
83 (* evaluation with freezed code context *) |
83 (* evaluation with freezed code context *) |