Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
eliminated hard tabs;
authorwenzelm
Fri, 22 Feb 2013 14:38:52 +0100
changeset 51239 67cc209493b2
parent 51238 20234cf043d1
child 51240 a7a04b449e8b
eliminated hard tabs;
src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML file | annotate | diff | comparison | revisions
src/Pure/Isar/toplevel.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Fri Feb 22 14:25:52 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Fri Feb 22 14:38:52 2013 +0100
@@ -8,7 +8,7 @@
 
 signature SLEDGEHAMMER_PROOF =
 sig
-	type label = string * int
+  type label = string * int
   type facts = label list * string list
 
   datatype isar_qualifier = Show | Then
--- a/src/Pure/Isar/toplevel.ML	Fri Feb 22 14:25:52 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML	Fri Feb 22 14:38:52 2013 +0100
@@ -721,7 +721,7 @@
         val estimate = fold (curry Time.+ o get_timing) proof_trs Time.zeroTime;
         val pri =
           if estimate = Time.zeroTime then ~1
-	  else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
+          else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
 
         val future_proof = Proof.global_future_proof
           (fn prf =>
isabelle