equal
deleted
inserted
replaced
51 |
51 |
52 |
52 |
53 (* evaluation with dynamic code context *) |
53 (* evaluation with dynamic code context *) |
54 |
54 |
55 fun dynamic_conv thy = Code_Thingol.dynamic_conv thy |
55 fun dynamic_conv thy = Code_Thingol.dynamic_conv thy |
56 (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program); |
56 (fn _ => fn program => fn _ => fn _ => rewrite_modulo thy NONE program); |
57 |
57 |
58 fun dynamic_tac thy = CONVERSION (dynamic_conv thy) THEN' conclude_tac thy NONE; |
58 fun dynamic_tac thy = CONVERSION (dynamic_conv thy) THEN' conclude_tac thy NONE; |
59 |
59 |
60 fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv thy o Thm.cterm_of thy; |
60 fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv thy o Thm.cterm_of thy; |
61 |
61 |