changeset 46947 | b8c7eb0c2f89 |
parent 46909 | 3c73a121a387 |
child 46949 | 94aa7b81bcf6 |
--- a/src/HOL/Tools/Quotient/quotient_type.ML Thu Mar 15 17:45:54 2012 +0100 +++ b/src/HOL/Tools/Quotient/quotient_type.ML Thu Mar 15 19:02:34 2012 +0100 @@ -272,8 +272,6 @@ (Parse.$$$ "/" |-- (partial -- Parse.term)) -- Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding))) -val _ = Keyword.keyword "/" - val _ = Outer_Syntax.local_theory_to_proof "quotient_type" "quotient type definitions (require equivalence proofs)"