equal
deleted
inserted
replaced
56 |
56 |
57 fun dynamic_tac thy = CONVERSION (dynamic_conv thy) THEN' conclude_tac thy NONE; |
57 fun dynamic_tac thy = CONVERSION (dynamic_conv thy) THEN' conclude_tac thy NONE; |
58 |
58 |
59 fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv thy o Thm.cterm_of thy; |
59 fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv thy o Thm.cterm_of thy; |
60 |
60 |
61 val setup = Method.setup (Binding.name "code_simp") |
61 val setup = |
62 (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac o Proof_Context.theory_of))) |
62 Method.setup @{binding code_simp} |
63 "simplification with code equations" |
63 (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac o Proof_Context.theory_of))) |
|
64 "simplification with code equations" |
64 #> Value.add_evaluator ("simp", dynamic_value o Proof_Context.theory_of); |
65 #> Value.add_evaluator ("simp", dynamic_value o Proof_Context.theory_of); |
65 |
66 |
66 |
67 |
67 (* evaluation with static code context *) |
68 (* evaluation with static code context *) |
68 |
69 |