author | blanchet |
Sat, 11 Sep 2010 12:30:50 +0200 | |
changeset 39325 | 5208954d906c |
parent 39324 | 05452dd66b2b |
child 39326 | 0b68add21e3d |
--- a/src/HOL/Tools/ATP/atp_systems.ML Sat Sep 11 10:35:00 2010 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Sat Sep 11 12:30:50 2010 +0200 @@ -122,10 +122,6 @@ priority ("Available ATPs: " ^ commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".") -fun available_atps thy = - priority ("Available ATPs: " ^ - commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".") - fun to_secs bonus time = (Time.toMilliseconds time + bonus + 999) div 1000 (* E prover *)