eliminated hard tabs;
authorwenzelm
Fri Feb 22 14:38:52 2013 +0100 (2013-02-22 ago)
changeset 5123967cc209493b2
parent 51238 20234cf043d1
child 51240 a7a04b449e8b
eliminated hard tabs;
src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Fri Feb 22 14:25:52 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Fri Feb 22 14:38:52 2013 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  signature SLEDGEHAMMER_PROOF =
     1.6  sig
     1.7 -	type label = string * int
     1.8 +  type label = string * int
     1.9    type facts = label list * string list
    1.10  
    1.11    datatype isar_qualifier = Show | Then
     2.1 --- a/src/Pure/Isar/toplevel.ML	Fri Feb 22 14:25:52 2013 +0100
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Feb 22 14:38:52 2013 +0100
     2.3 @@ -721,7 +721,7 @@
     2.4          val estimate = fold (curry Time.+ o get_timing) proof_trs Time.zeroTime;
     2.5          val pri =
     2.6            if estimate = Time.zeroTime then ~1
     2.7 -	  else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
     2.8 +          else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
     2.9  
    2.10          val future_proof = Proof.global_future_proof
    2.11            (fn prf =>