src/HOL/HOLCF/IOA/NTP/Impl.thy
changeset 45620 f2a587696afb
parent 42151 4da4fc77664b
child 51717 9e7d1c139569
     1.1 --- a/src/HOL/HOLCF/IOA/NTP/Impl.thy	Wed Nov 23 22:07:55 2011 +0100
     1.2 +++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy	Wed Nov 23 22:59:39 2011 +0100
     1.3 @@ -105,8 +105,10 @@
     1.4  val ss = @{simpset} addsimps @{thms "transitions"};
     1.5  val rename_ss = ss addsimps @{thms unfold_renaming};
     1.6  
     1.7 -val tac     = asm_simp_tac (ss addcongs [@{thm conj_cong}] addsplits [@{thm split_if}])
     1.8 -val tac_ren = asm_simp_tac (rename_ss addcongs [@{thm conj_cong}] addsplits [@{thm split_if}])
     1.9 +val tac =
    1.10 +  asm_simp_tac (ss |> Simplifier.add_cong @{thm conj_cong} |> Splitter.add_split @{thm split_if})
    1.11 +val tac_ren =
    1.12 +  asm_simp_tac (rename_ss |> Simplifier.add_cong @{thm conj_cong} |> Splitter.add_split @{thm split_if})
    1.13  *}
    1.14  
    1.15