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