src/HOL/ex/SVC_Oracle.thy
changeset 28263 69eaa97e7e96
parent 25929 6bfef23e26be
child 28290 4cc2b6046258
     1.1 --- a/src/HOL/ex/SVC_Oracle.thy	Wed Sep 17 21:27:08 2008 +0200
     1.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Wed Sep 17 21:27:14 2008 +0200
     1.3 @@ -116,11 +116,6 @@
     1.4      val th = svc_oracle (Thm.theory_of_thm st) abs_goal
     1.5     in compose_tac (false, th, 0) i st end
     1.6     handle TERM _ => no_tac st;
     1.7 -
     1.8 -
     1.9 -(*check if user has SVC installed*)
    1.10 -fun svc_enabled () = getenv "SVC_HOME" <> "";
    1.11 -fun if_svc_enabled f x = if svc_enabled () then f x else ();
    1.12  *}
    1.13  
    1.14  end