equal
deleted
inserted
replaced
17 |
17 |
18 (* wrapper for define *) |
18 (* wrapper for define *) |
19 fun define name mx attr rhs lthy = |
19 fun define name mx attr rhs lthy = |
20 let |
20 let |
21 val ((rhs, (_ , thm)), lthy') = |
21 val ((rhs, (_ , thm)), lthy') = |
22 Local_Theory.define "" ((name, mx), (attr, rhs)) lthy |
22 Local_Theory.define ((name, mx), (attr, rhs)) lthy |
23 in |
23 in |
24 ((rhs, thm), lthy') |
24 ((rhs, thm), lthy') |
25 end |
25 end |
26 |
26 |
27 datatype flag = absF | repF |
27 datatype flag = absF | repF |