src/HOLCF/IOA/Modelcheck/MuIOA.thy
changeset 37140 6ba1b0ef0cc4
parent 32960 69916a850301
child 37391 476270a6c2dc
     1.1 --- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Wed May 26 16:31:44 2010 +0200
     1.2 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Wed May 26 16:44:57 2010 +0200
     1.3 @@ -276,13 +276,13 @@
     1.4  OldGoals.by (REPEAT (dtac eq_reflection 1));
     1.5  (* Bis hierher wird im Kapitel 4 erl"autert, ab hier im Kapitel 5 *)
     1.6  OldGoals.by (full_simp_tac ((global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs)
     1.7 -                              delsimps [not_iff,split_part])
     1.8 +                              delsimps [not_iff, @{thm split_part}])
     1.9                                addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @
    1.10                                          rename_simps @ ioa_simps @ asig_simps)) 1);
    1.11  OldGoals.by (full_simp_tac
    1.12 -  (Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1);
    1.13 +  (Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff, @{thm split_part}]) 1);
    1.14  OldGoals.by (REPEAT (if_full_simp_tac
    1.15 -  (global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1));
    1.16 +  (global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff, @{thm split_part}]) 1));
    1.17  OldGoals.by (call_mucke_tac 1);
    1.18  (* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *)
    1.19  OldGoals.by (atac 1);