equal
deleted
inserted
replaced
263 |
263 |
264 fun is_eq (Const (@{const_name "op ="}, _)) = true |
264 fun is_eq (Const (@{const_name "op ="}, _)) = true |
265 | is_eq _ = false |
265 | is_eq _ = false |
266 |
266 |
267 fun mk_rel_compose (trm1, trm2) = |
267 fun mk_rel_compose (trm1, trm2) = |
268 Const (@{const_name "rel_conj"}, dummyT) $ trm1 $ trm2 |
268 Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2 |
269 |
269 |
270 fun get_relmap ctxt s = |
270 fun get_relmap ctxt s = |
271 let |
271 let |
272 val thy = ProofContext.theory_of ctxt |
272 val thy = ProofContext.theory_of ctxt |
273 val exn = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")") |
273 val exn = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")") |