src/HOLCF/IOA/meta_theory/CompoTraces.thy
changeset 26339 7825c83c9eff
parent 19741 f65265d71426
child 26359 6d437bde2f1d
equal deleted inserted replaced
26338:f8ed02f22433 26339:7825c83c9eff
    66 
    66 
    67 finiteR_mksch:
    67 finiteR_mksch:
    68   "Finite (mksch A B$tr$x$y) --> Finite tr"
    68   "Finite (mksch A B$tr$x$y) --> Finite tr"
    69 
    69 
    70 
    70 
    71 ML_setup {* change_simpset (fn ss => ss setmksym (K NONE)) *}
    71 declaration {* fn _ => Simplifier.map_ss (fn ss => ss setmksym (K NONE)) *}
    72 
    72 
    73 
    73 
    74 subsection "mksch rewrite rules"
    74 subsection "mksch rewrite rules"
    75 
    75 
    76 lemma mksch_unfold:
    76 lemma mksch_unfold:
   965 apply (rule set_ext)
   965 apply (rule set_ext)
   966 apply (simp add: compositionality_tr externals_of_par)
   966 apply (simp add: compositionality_tr externals_of_par)
   967 done
   967 done
   968 
   968 
   969 
   969 
   970 ML_setup {* change_simpset (fn ss => ss setmksym (SOME o symmetric_fun)) *}
   970 declaration {* fn _ => Simplifier.map_ss (fn ss => ss setmksym (SOME o symmetric_fun)) *}
   971 
   971 
   972 
   972 
   973 end
   973 end