equal
deleted
inserted
replaced
26 |
26 |
27 (** interface and syntax setup **) |
27 (** interface and syntax setup **) |
28 |
28 |
29 (* the ML-interface takes |
29 (* the ML-interface takes |
30 |
30 |
31 - the mixfix annotation |
31 - the mixfix annotation |
32 - name and attributes |
32 - name and attributes |
33 - the new constant as term |
33 - the new constant as term |
34 - the rhs of the definition as term |
34 - the rhs of the definition as term |
35 |
35 |
36 it returns the defined constant and its definition |
36 it returns the defined constant and its definition |
37 theorem; stores the data in the qconsts slot *) |
37 theorem; stores the data in the qconsts slot |
38 |
38 *) |
39 fun quotient_def mx attr lhs rhs lthy = |
39 fun quotient_def mx attr lhs rhs lthy = |
40 let |
40 let |
41 val Free (lhs_str, lhs_ty) = lhs; (* FIXME/TODO: this throws an excpt., if the const is already def.*) |
41 val Free (lhs_str, lhs_ty) = lhs; (* FIXME/TODO: this throws an excpt., if the const is already def.*) |
42 val qconst_bname = Binding.name lhs_str; |
42 val qconst_bname = Binding.name lhs_str; |
43 val absrep_trm = absrep_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs |
43 val absrep_trm = absrep_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs |