equal
deleted
inserted
replaced
82 |
82 |
83 |
83 |
84 (* evaluation with freezed code context *) |
84 (* evaluation with freezed code context *) |
85 |
85 |
86 fun static_eval_conv thy some_ss consts = no_frees_conv |
86 fun static_eval_conv thy some_ss consts = no_frees_conv |
87 (Code_Thingol.static_eval_conv_simple thy consts (rewrite_modulo thy some_ss)); |
87 (Code_Thingol.static_eval_conv_simple thy consts |
|
88 (fn program => fn thy => rewrite_modulo thy some_ss program)); |
88 |
89 |
89 fun static_eval_tac thy some_ss consts = CONVERSION (static_eval_conv thy some_ss consts) |
90 fun static_eval_tac thy some_ss consts = CONVERSION (static_eval_conv thy some_ss consts) |
90 THEN' conclude_tac thy some_ss; |
91 THEN' conclude_tac thy some_ss; |
91 |
92 |
92 end; |
93 end; |