equal
deleted
inserted
replaced
349 |
349 |
350 fun normalization_oracle (thy, Normalization (code, t, t')) = |
350 fun normalization_oracle (thy, Normalization (code, t, t')) = |
351 Logic.mk_equals (t, eval thy code t t'); |
351 Logic.mk_equals (t, eval thy code t t'); |
352 |
352 |
353 fun normalization_invoke thy code t t' = |
353 fun normalization_invoke thy code t t' = |
354 Thm.invoke_oracle_i thy "Nbe.normalization" (thy, Normalization (code, t, t')); |
354 Thm.invoke_oracle_i thy "HOL.normalization" (thy, Normalization (code, t, t')); |
|
355 (*FIXME get rid of hardwired theory name "HOL"*) |
355 |
356 |
356 fun normalization_conv ct = |
357 fun normalization_conv ct = |
357 let |
358 let |
358 val thy = Thm.theory_of_cterm ct; |
359 val thy = Thm.theory_of_cterm ct; |
359 fun conv code t' ct = |
360 fun conv code t' ct = |