tuned
authorbulwahn
Fri, 03 Dec 2010 08:40:47 +0100
changeset 40902 7c652e4a924a
parent 40901 8fdfa9c4e7ed
child 40903 1332f6e856b9
tuned
src/HOL/Tools/inductive.ML
--- 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