some minor tunings
authorurbanc
Sun, 27 Nov 2005 05:09:43 +0100
changeset 18265 f3f81becc1f1
parent 18264 3b808e24667b
child 18266 55c201fe4c95
some minor tunings
src/HOL/Nominal/nominal_induct.ML
--- 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;