| changeset 40902 | 7c652e4a924a |
| parent 40316 | 665862241968 |
| child 41075 | 4bed56dc95fb |
--- a/src/HOL/Tools/inductive.ML Fri Dec 03 08:40:46 2010 +0100 +++ b/src/HOL/Tools/inductive.ML Fri Dec 03 08:40:47 2010 +0100 @@ -596,7 +596,7 @@ val inductive_simps = gen_inductive_simps Attrib.intern_src Syntax.read_prop; val inductive_simps_i = gen_inductive_simps (K I) Syntax.check_prop; - + (* prove induction rule *) fun prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono