equal
deleted
inserted
replaced
266 val enriched_type = gen_enriched_type Syntax.check_term; |
266 val enriched_type = gen_enriched_type Syntax.check_term; |
267 val enriched_type_cmd = gen_enriched_type Syntax.read_term; |
267 val enriched_type_cmd = gen_enriched_type Syntax.read_term; |
268 |
268 |
269 val _ = Outer_Syntax.local_theory_to_proof "enriched_type" |
269 val _ = Outer_Syntax.local_theory_to_proof "enriched_type" |
270 "register operations managing the functorial structure of a type" |
270 "register operations managing the functorial structure of a type" |
271 Keyword.thy_goal (Scan.option (Parse.name --| Parse.$$$ ":") -- Parse.term |
271 Keyword.thy_goal (Scan.option (Parse.name --| @{keyword ":"}) -- Parse.term |
272 >> (fn (prfx, t) => enriched_type_cmd prfx t)); |
272 >> (fn (prfx, t) => enriched_type_cmd prfx t)); |
273 |
273 |
274 end; |
274 end; |