equal
deleted
inserted
replaced
135 end |
135 end |
136 |
136 |
137 |
137 |
138 section {* type definition for the quotient type *} |
138 section {* type definition for the quotient type *} |
139 |
139 |
|
140 ML {* Proof.theorem_i NONE *} |
|
141 |
140 use "quotient.ML" |
142 use "quotient.ML" |
141 |
143 |
142 declare [[map list = (map, LIST_REL)]] |
144 declare [[map list = (map, LIST_REL)]] |
143 declare [[map * = (prod_fun, prod_rel)]] |
145 declare [[map * = (prod_fun, prod_rel)]] |
144 declare [[map "fun" = (fun_map, FUN_REL)]] |
146 declare [[map "fun" = (fun_map, FUN_REL)]] |
148 ML {* maps_lookup @{theory} "fun" *} |
150 ML {* maps_lookup @{theory} "fun" *} |
149 |
151 |
150 ML {* |
152 ML {* |
151 val quot_def_parser = |
153 val quot_def_parser = |
152 (OuterParse.$$$ "(" |-- OuterParse.$$$ "with" |-- |
154 (OuterParse.$$$ "(" |-- OuterParse.$$$ "with" |-- |
153 ((OuterParse.list1 OuterParse.binding) --| OuterParse.$$$ ")")) -- |
155 ((OuterParse.list1 OuterParse.typ) --| OuterParse.$$$ ")")) -- |
154 (OuterParse.binding -- |
156 (OuterParse.binding -- |
155 Scan.option (OuterParse.$$$ "::" |-- OuterParse.typ) -- |
157 Scan.option (OuterParse.$$$ "::" |-- OuterParse.typ) -- |
156 OuterParse.mixfix --| OuterParse.where_ -- SpecParse.spec) |
158 OuterParse.mixfix --| OuterParse.where_ -- SpecParse.spec) |
157 *} |
159 *} |
158 |
160 |