equal
deleted
inserted
replaced
288 |
288 |
289 (* outer syntax *) |
289 (* outer syntax *) |
290 |
290 |
291 val hints = |
291 val hints = |
292 @{keyword "("} |-- |
292 @{keyword "("} |-- |
293 Parse.!!! (Parse.position (@{keyword "hints"} -- Args.parse) --| @{keyword ")"}) >> Args.src; |
293 Parse.!!! (Parse.position @{keyword "hints"} -- Args.parse --| @{keyword ")"}) |
|
294 >> uncurry Args.src; |
294 |
295 |
295 val recdef_decl = |
296 val recdef_decl = |
296 Scan.optional |
297 Scan.optional |
297 (@{keyword "("} -- Parse.!!! (@{keyword "permissive"} -- @{keyword ")"}) >> K false) true -- |
298 (@{keyword "("} -- Parse.!!! (@{keyword "permissive"} -- @{keyword ")"}) >> K false) true -- |
298 Parse.name -- Parse.term -- Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop) |
299 Parse.name -- Parse.term -- Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop) |