equal
deleted
inserted
replaced
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 a 4-tuple consisting of *) |
30 (* *) |
30 (* *) |
31 (* - the mixfix annotation *) |
31 (* - the mixfix annotation *) |
32 (* - name and attributes *) |
32 (* - name and attributes *) |
33 (* - the new constant including its type *) |
33 (* - the new constant as term *) |
34 (* - the rhs of the definition *) |
34 (* - the rhs of the definition as term *) |
35 (* *) |
35 (* *) |
36 (* 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; |
53 (fn phi => qconsts_update_gen lhs_str (qcinfo phi)) lthy' |
53 (fn phi => qconsts_update_gen lhs_str (qcinfo phi)) lthy' |
54 in |
54 in |
55 ((trm, thm), lthy'') |
55 ((trm, thm), lthy'') |
56 end |
56 end |
57 |
57 |
58 fun quotdef_cmd ((attr, lhsstr), (mx, rhsstr)) lthy = |
58 fun quotdef_cmd ((attr, lhs_str), (mx, rhs_str)) lthy = |
59 let |
59 let |
60 val lhs = Syntax.read_term lthy lhsstr |
60 val lhs = Syntax.read_term lthy lhs_str |
61 val rhs = Syntax.read_term lthy rhsstr |
61 val rhs = Syntax.read_term lthy rhs_str |
62 in |
62 in |
63 quotient_def mx attr lhs rhs lthy |> snd |
63 quotient_def mx attr lhs rhs lthy |> snd |
64 end |
64 end |
65 |
65 |
66 val _ = OuterKeyword.keyword "as"; |
66 val _ = OuterKeyword.keyword "as"; |