Phil:
>When a theorem is proven and HOL Light announces "no
>subgoals", there is no jingle. or musical fanfare. Please
>fix.
How about?
let e tac =
let gs = refine(by(VALID tac)) in
match gs with
| (_,gls,_)::_ ->
if length gls = 0
then let _ = Unix.system ("mpg123 -q "^(!hol_dir)^"/ahhh.mp3") in gs
else gs
| _ -> gs;;
(I'm sure this can be shorter, but who cares.)
For the sound file (which you need to put in the HOL Light
directory): <http://www.cs.ru.nl/~freek/pics/ahhh.mp3>
Bonus points for people who know where this sound came from.
Freek
------------------------------------------------------------------------------
Master SQL Server Development, Administration, T-SQL, SSAS, SSIS, SSRS
and more. Get SQL Server skills now (including 2012) with LearnDevNow -
200+ hours of step-by-step video tutorials by Microsoft MVPs and experts.
SALE $99.99 this month only - learn more at:
http://p.sf.net/sfu/learnmore_122512
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
