moved global ML bindings to global place;
authorwenzelm
Wed Sep 17 21:27:14 2008 +0200 (2008-09-17)
changeset 2826369eaa97e7e96
parent 28262 aa7ca36d67fd
child 28264 e1dae766c108
moved global ML bindings to global place;
src/HOL/Main.thy
src/HOL/Modelcheck/EindhovenSyn.thy
src/HOL/Modelcheck/MuckeSyn.thy
src/HOL/Modelcheck/ROOT.ML
src/HOL/ROOT.ML
src/HOL/ex/ROOT.ML
src/HOL/ex/SVC_Oracle.thy
src/HOLCF/IOA/Modelcheck/ROOT.ML
     1.1 --- a/src/HOL/Main.thy	Wed Sep 17 21:27:08 2008 +0200
     1.2 +++ b/src/HOL/Main.thy	Wed Sep 17 21:27:14 2008 +0200
     1.3 @@ -8,8 +8,6 @@
     1.4  imports Plain Code_Eval Map Nat_Int_Bij Recdef
     1.5  begin
     1.6  
     1.7 -ML {* val HOL_proofs = ! Proofterm.proofs *}
     1.8 -
     1.9  text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
    1.10  
    1.11  end
     2.1 --- a/src/HOL/Modelcheck/EindhovenSyn.thy	Wed Sep 17 21:27:08 2008 +0200
     2.2 +++ b/src/HOL/Modelcheck/EindhovenSyn.thy	Wed Sep 17 21:27:14 2008 +0200
     2.3 @@ -73,10 +73,6 @@
     2.4  
     2.5  val Eindhoven_ss =
     2.6    @{simpset} addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
     2.7 -
     2.8 -(*check if user has pmu installed*)
     2.9 -fun eindhoven_enabled () = getenv "EINDHOVEN_HOME" <> "";
    2.10 -fun if_eindhoven_enabled f x = if eindhoven_enabled () then f x else ();
    2.11  *}
    2.12  
    2.13  end
     3.1 --- a/src/HOL/Modelcheck/MuckeSyn.thy	Wed Sep 17 21:27:08 2008 +0200
     3.2 +++ b/src/HOL/Modelcheck/MuckeSyn.thy	Wed Sep 17 21:27:14 2008 +0200
     3.3 @@ -236,11 +236,6 @@
     3.4          full_simp_tac (Mucke_ss delsimps [not_iff,split_part]) i,
     3.5          move_mus i, call_mucke_tac i,atac i,
     3.6          REPEAT (rtac refl i)] state);
     3.7 -
     3.8 -(*check if user has mucke installed*)
     3.9 -fun mucke_enabled () = getenv "MUCKE_HOME" <> "";
    3.10 -fun if_mucke_enabled f x = if mucke_enabled () then f x else ();
    3.11 -
    3.12  *}
    3.13  
    3.14  end
     4.1 --- a/src/HOL/Modelcheck/ROOT.ML	Wed Sep 17 21:27:08 2008 +0200
     4.2 +++ b/src/HOL/Modelcheck/ROOT.ML	Wed Sep 17 21:27:14 2008 +0200
     4.3 @@ -10,6 +10,10 @@
     4.4  
     4.5  (* Einhoven model checker *)
     4.6  
     4.7 +(*check if user has pmu installed*)
     4.8 +fun eindhoven_enabled () = getenv "EINDHOVEN_HOME" <> "";
     4.9 +fun if_eindhoven_enabled f x = if eindhoven_enabled () then f x else ();
    4.10 +
    4.11  time_use_thy "EindhovenSyn";
    4.12  if_eindhoven_enabled time_use_thy "EindhovenExample";
    4.13  
    4.14 @@ -18,5 +22,9 @@
    4.15  
    4.16  time_use_thy "MuckeSyn";
    4.17  
    4.18 +(*check if user has mucke installed*)
    4.19 +fun mucke_enabled () = getenv "MUCKE_HOME" <> "";
    4.20 +fun if_mucke_enabled f x = if mucke_enabled () then f x else ();
    4.21 +
    4.22  if_mucke_enabled time_use_thy "MuckeExample1";
    4.23  if_mucke_enabled time_use_thy "MuckeExample2";
     5.1 --- a/src/HOL/ROOT.ML	Wed Sep 17 21:27:08 2008 +0200
     5.2 +++ b/src/HOL/ROOT.ML	Wed Sep 17 21:27:14 2008 +0200
     5.3 @@ -5,3 +5,6 @@
     5.4  *)
     5.5  
     5.6  use_thy "Complex/Complex_Main";
     5.7 +
     5.8 +val HOL_proofs = ! Proofterm.proofs;
     5.9 +
     6.1 --- a/src/HOL/ex/ROOT.ML	Wed Sep 17 21:27:08 2008 +0200
     6.2 +++ b/src/HOL/ex/ROOT.ML	Wed Sep 17 21:27:14 2008 +0200
     6.3 @@ -72,6 +72,11 @@
     6.4  time_use_thy "Reflection";
     6.5  
     6.6  time_use_thy "SVC_Oracle";
     6.7 +
     6.8 +(*check if user has SVC installed*)
     6.9 +fun svc_enabled () = getenv "SVC_HOME" <> "";
    6.10 +fun if_svc_enabled f x = if svc_enabled () then f x else ();
    6.11 +
    6.12  if_svc_enabled time_use_thy "svc_test";
    6.13  
    6.14  (* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *)
     7.1 --- a/src/HOL/ex/SVC_Oracle.thy	Wed Sep 17 21:27:08 2008 +0200
     7.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Wed Sep 17 21:27:14 2008 +0200
     7.3 @@ -116,11 +116,6 @@
     7.4      val th = svc_oracle (Thm.theory_of_thm st) abs_goal
     7.5     in compose_tac (false, th, 0) i st end
     7.6     handle TERM _ => no_tac st;
     7.7 -
     7.8 -
     7.9 -(*check if user has SVC installed*)
    7.10 -fun svc_enabled () = getenv "SVC_HOME" <> "";
    7.11 -fun if_svc_enabled f x = if svc_enabled () then f x else ();
    7.12  *}
    7.13  
    7.14  end
     8.1 --- a/src/HOLCF/IOA/Modelcheck/ROOT.ML	Wed Sep 17 21:27:08 2008 +0200
     8.2 +++ b/src/HOLCF/IOA/Modelcheck/ROOT.ML	Wed Sep 17 21:27:14 2008 +0200
     8.3 @@ -7,6 +7,10 @@
     8.4  
     8.5  with_path "../../../HOL/Modelcheck" time_use_thy "MuIOAOracle";
     8.6  
     8.7 +(*check if user has mucke installed*)
     8.8 +fun mucke_enabled () = getenv "MUCKE_HOME" <> "";
     8.9 +fun if_mucke_enabled f x = if mucke_enabled () then f x else ();
    8.10 +
    8.11  (*examples*)
    8.12  if_mucke_enabled time_use_thy "Cockpit";
    8.13  if_mucke_enabled time_use_thy "Ring3";