equal
deleted
inserted
replaced
297 |
297 |
298 |
298 |
299 |
299 |
300 (** outer syntax **) |
300 (** outer syntax **) |
301 |
301 |
302 val _ = Keyword.keyword "morphisms"; |
|
303 |
|
304 val _ = |
302 val _ = |
305 Outer_Syntax.local_theory_to_proof "typedef" "HOL type definition (requires non-emptiness proof)" |
303 Outer_Syntax.local_theory_to_proof "typedef" "HOL type definition (requires non-emptiness proof)" |
306 Keyword.thy_goal |
304 Keyword.thy_goal |
307 (Scan.optional (Parse.$$$ "(" |-- |
305 (Scan.optional (Parse.$$$ "(" |-- |
308 ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding || |
306 ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding || |