equal
deleted
inserted
replaced
16 |
16 |
17 (* wrappers for define, note and theorem_i *) |
17 (* wrappers for define, note and theorem_i *) |
18 fun define (name, mx, rhs) lthy = |
18 fun define (name, mx, rhs) lthy = |
19 let |
19 let |
20 val ((rhs, (_ , thm)), lthy') = |
20 val ((rhs, (_ , thm)), lthy') = |
21 Local_Theory.define "" ((name, mx), (Attrib.empty_binding, rhs)) lthy |
21 Local_Theory.define ((name, mx), (Attrib.empty_binding, rhs)) lthy |
22 in |
22 in |
23 ((rhs, thm), lthy') |
23 ((rhs, thm), lthy') |
24 end |
24 end |
25 |
25 |
26 fun note (name, thm) lthy = |
26 fun note (name, thm) lthy = |