equal
deleted
inserted
replaced
37 in |
37 in |
38 Proof.theorem_i NONE after_qed' [goals'] ctxt |
38 Proof.theorem_i NONE after_qed' [goals'] ctxt |
39 end |
39 end |
40 |
40 |
41 |
41 |
42 (* definition of the quotient type *) |
42 (* definition of quotient types *) |
43 (***********************************) |
43 (********************************) |
44 |
44 |
45 (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *) |
45 (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *) |
46 fun typedef_term rel rty lthy = |
46 fun typedef_term rel rty lthy = |
47 let |
47 let |
48 val [x, c] = [("x", rty), ("c", HOLogic.mk_setT rty)] |
48 val [x, c] = [("x", rty), ("c", HOLogic.mk_setT rty)] |