equal
deleted
inserted
replaced
22 in |
22 in |
23 ((rhs, thm), lthy') |
23 ((rhs, thm), lthy') |
24 end |
24 end |
25 |
25 |
26 |
26 |
27 (* interface and syntax setup *) |
27 (** interface and syntax setup **) |
28 |
28 |
29 (* the ML-interface takes a 4-tuple consisting of *) |
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; |