author | bulwahn |
Fri, 03 Dec 2010 08:40:47 +0100 | |
changeset 40902 | 7c652e4a924a |
parent 40901 | 8fdfa9c4e7ed |
child 40903 | 1332f6e856b9 |
--- 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