author | urbanc |
Sun, 27 Nov 2005 05:09:43 +0100 | |
changeset 18265 | f3f81becc1f1 |
parent 18264 | 3b808e24667b |
child 18266 | 55c201fe4c95 |
--- a/src/HOL/Nominal/nominal_induct.ML Sun Nov 27 05:00:43 2005 +0100 +++ b/src/HOL/Nominal/nominal_induct.ML Sun Nov 27 05:09:43 2005 +0100 @@ -83,12 +83,5 @@ val nominal_induct_method = Method.RAW_METHOD_CASES o nominal_induct_tac oo (#2 oo Method.syntax nominal_induct_args); -(* nominal_induc_method needs to have the type - - Args.src -> Proof.context -> Proof.method - - CHECK THAT - -*) end;