do not open OldGoals;
authorwenzelm
Fri Jul 24 22:09:09 2009 +0200 (2009-07-24)
changeset 321780261c3eaae41
parent 32177 bc02c5bfcb5b
child 32179 1c9c991e41c0
do not open OldGoals;
src/HOL/Modelcheck/MuckeSyn.thy
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/ex/Meson_Test.thy
src/HOLCF/IOA/Modelcheck/MuIOA.thy
     1.1 --- a/src/HOL/Modelcheck/MuckeSyn.thy	Fri Jul 24 21:34:37 2009 +0200
     1.2 +++ b/src/HOL/Modelcheck/MuckeSyn.thy	Fri Jul 24 22:09:09 2009 +0200
     1.3 @@ -118,7 +118,7 @@
     1.4  
     1.5  local
     1.6  
     1.7 -  val move_thm = prove_goal @{theory} "[| a = b ==> P a; a = b |] ==> P b"
     1.8 +  val move_thm = OldGoals.prove_goal @{theory} "[| a = b ==> P a; a = b |] ==> P b"
     1.9  	(fn prems => [cut_facts_tac prems 1, dtac sym 1, hyp_subst_tac 1,
    1.10  		     REPEAT (resolve_tac prems 1)]);
    1.11  
    1.12 @@ -159,9 +159,9 @@
    1.13  
    1.14  (* transforming fun-defs into lambda-defs *)
    1.15  
    1.16 -val [eq] = goal Pure.thy "(!! x. f x == g x) ==> f == g";
    1.17 - by (rtac (extensional eq) 1);
    1.18 -qed "ext_rl";
    1.19 +val [eq] = OldGoals.goal Pure.thy "(!! x. f x == g x) ==> f == g";
    1.20 + OldGoals.by (rtac (extensional eq) 1);
    1.21 +OldGoals.qed "ext_rl";
    1.22  
    1.23  infix cc;
    1.24  
    1.25 @@ -196,7 +196,7 @@
    1.26  	val rhs = Syntax.string_of_term_global thy (freeze_thaw RHS)
    1.27  	val gl = delete_bold_string (fnam ^" == % " ^ (getargs LHS) ^" . " ^ rhs);
    1.28      in
    1.29 -	SOME (prove_goal thy gl (fn prems =>
    1.30 +	SOME (OldGoals.prove_goal thy gl (fn prems =>
    1.31    		[(REPEAT (rtac ext_rl 1)), (rtac t 1) ]))
    1.32      end
    1.33  | mk_lam_def [] _ t= NONE; 
     2.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Fri Jul 24 21:34:37 2009 +0200
     2.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Fri Jul 24 22:09:09 2009 +0200
     2.3 @@ -1,4 +1,3 @@
     2.4 -open OldGoals;
     2.5  
     2.6  val trace_mc = ref false; 
     2.7  
     2.8 @@ -110,9 +109,9 @@
     2.9  (
    2.10  OldGoals.push_proof();
    2.11  OldGoals.goalw_cterm [] (cterm_of sign trm);
    2.12 -by (simp_tac (global_simpset_of sign) 1);
    2.13 +OldGoals.by (simp_tac (global_simpset_of sign) 1);
    2.14          let
    2.15 -        val if_tmp_result = result()
    2.16 +        val if_tmp_result = OldGoals.result()
    2.17          in
    2.18          (
    2.19          OldGoals.pop_proof();
     3.1 --- a/src/HOL/ex/Meson_Test.thy	Fri Jul 24 21:34:37 2009 +0200
     3.2 +++ b/src/HOL/ex/Meson_Test.thy	Fri Jul 24 22:09:09 2009 +0200
     3.3 @@ -5,7 +5,11 @@
     3.4  imports Main
     3.5  begin
     3.6  
     3.7 -ML {* open OldGoals *}
     3.8 +ML {*
     3.9 +  val Goal = OldGoals.Goal;
    3.10 +  val by = OldGoals.by;
    3.11 +  val gethyps = OldGoals.gethyps;
    3.12 +*}
    3.13  
    3.14  text {*
    3.15    WARNING: there are many potential conflicts between variables used
     4.1 --- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Fri Jul 24 21:34:37 2009 +0200
     4.2 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Fri Jul 24 22:09:09 2009 +0200
     4.3 @@ -246,7 +246,7 @@
     4.4  in
     4.5  (
     4.6  OldGoals.push_proof();
     4.7 -Goal 
     4.8 +OldGoals.Goal 
     4.9  ( "(Internal_of_A = (% a::(" ^ action_type_str ^ "). a:(" ^ ia_str^
    4.10    "))) --> (Internal_of_C = (% a::(" ^ action_type_str ^ "). a:(" ^ ic_str ^ 
    4.11    "))) --> (Start_of_A = (% (" ^ abs_pre_tupel_typed ^
    4.12 @@ -275,21 +275,21 @@
    4.13   ") --> (! " ^ con_pre_str_typed ^ ". ! " ^ abs_pre_str_typed ^
    4.14  	". (Start_of_C (" ^ con_pre_tupel ^ ") & Start_of_A (" ^ abs_pre_tupel ^
    4.15  	")) --> isSimCA(" ^ con_pre_tupel ^ "," ^ abs_pre_tupel ^ "))");
    4.16 -by (REPEAT (rtac impI 1));
    4.17 -by (REPEAT (dtac eq_reflection 1));
    4.18 +OldGoals.by (REPEAT (rtac impI 1));
    4.19 +OldGoals.by (REPEAT (dtac eq_reflection 1));
    4.20  (* Bis hierher wird im Kapitel 4 erl"autert, ab hier im Kapitel 5 *)
    4.21 -by (full_simp_tac ((global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs)
    4.22 +OldGoals.by (full_simp_tac ((global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs)
    4.23                                delsimps [not_iff,split_part])
    4.24  			      addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @
    4.25                                          rename_simps @ ioa_simps @ asig_simps)) 1);
    4.26 -by (full_simp_tac
    4.27 +OldGoals.by (full_simp_tac
    4.28    (Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1);
    4.29 -by (REPEAT (if_full_simp_tac
    4.30 +OldGoals.by (REPEAT (if_full_simp_tac
    4.31    (global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1));
    4.32 -by (call_mucke_tac 1);
    4.33 +OldGoals.by (call_mucke_tac 1);
    4.34  (* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *)
    4.35 -by (atac 1);
    4.36 -result();
    4.37 +OldGoals.by (atac 1);
    4.38 +OldGoals.result();
    4.39  OldGoals.pop_proof();
    4.40  Thm.cterm_of sign (Logic.strip_imp_concl subgoal)
    4.41  )