equal
deleted
inserted
replaced
698 val liftdef_parser = |
698 val liftdef_parser = |
699 (((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix')) >> Parse.triple2) |
699 (((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix')) >> Parse.triple2) |
700 --| @{keyword "is"} -- Parse.term -- |
700 --| @{keyword "is"} -- Parse.term -- |
701 Scan.optional (@{keyword "parametric"} |-- Parse.!!! Parse.xthms1) []) >> Parse.triple1 |
701 Scan.optional (@{keyword "parametric"} |-- Parse.!!! Parse.xthms1) []) >> Parse.triple1 |
702 val _ = |
702 val _ = |
703 Outer_Syntax.local_theory_to_proof @{command_spec "lift_definition"} |
703 Outer_Syntax.local_theory_to_proof @{command_keyword lift_definition} |
704 "definition for constants over the quotient type" |
704 "definition for constants over the quotient type" |
705 (liftdef_parser >> lift_def_cmd_with_err_handling) |
705 (liftdef_parser >> lift_def_cmd_with_err_handling) |
706 |
706 |
707 |
707 |
708 end (* structure *) |
708 end (* structure *) |