equal
deleted
inserted
replaced
10 local_theory -> local_theory |
10 local_theory -> local_theory |
11 end; |
11 end; |
12 |
12 |
13 structure Quotient_Def: QUOTIENT_DEF = |
13 structure Quotient_Def: QUOTIENT_DEF = |
14 struct |
14 struct |
|
15 |
|
16 open Quotient_Info; |
|
17 open Quotient_Type; |
15 |
18 |
16 (* wrapper for define *) |
19 (* wrapper for define *) |
17 fun define name mx attr rhs lthy = |
20 fun define name mx attr rhs lthy = |
18 let |
21 let |
19 val ((rhs, (_ , thm)), lthy') = |
22 val ((rhs, (_ , thm)), lthy') = |
127 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants" |
130 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants" |
128 OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd) |
131 OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd) |
129 |
132 |
130 end; (* structure *) |
133 end; (* structure *) |
131 |
134 |
132 open Quotient_Def; |
|
133 |
135 |
134 |
136 |
|
137 |