src/HOL/Tools/inductive.ML
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