equal
deleted
inserted
replaced
464 end; |
464 end; |
465 |
465 |
466 (* evaluation oracle *) |
466 (* evaluation oracle *) |
467 |
467 |
468 val (_, norm_oracle) = Context.>>> (Context.map_theory_result |
468 val (_, norm_oracle) = Context.>>> (Context.map_theory_result |
469 (Thm.add_oracle ("norm", fn (thy, t, naming, program, vs_ty_t, deps) => |
469 (Thm.add_oracle (Binding.name "norm", fn (thy, t, naming, program, vs_ty_t, deps) => |
470 Thm.cterm_of thy (Logic.mk_equals (t, eval thy t naming program vs_ty_t deps))))); |
470 Thm.cterm_of thy (Logic.mk_equals (t, eval thy t naming program vs_ty_t deps))))); |
471 |
471 |
472 fun add_triv_classes thy = |
472 fun add_triv_classes thy = |
473 let |
473 let |
474 val inters = curry (Sorts.inter_sort (Sign.classes_of thy)) |
474 val inters = curry (Sorts.inter_sort (Sign.classes_of thy)) |