src/HOLCF/IOA/meta_theory/Traces.thy
changeset 26339 7825c83c9eff
parent 22808 a7daa74e2980
child 26359 6d437bde2f1d
equal deleted inserted replaced
26338:f8ed02f22433 26339:7825c83c9eff
   193   "Traces A == (traces A,asig_of A)"
   193   "Traces A == (traces A,asig_of A)"
   194 
   194 
   195 
   195 
   196 lemmas [simp del] = ex_simps all_simps split_paired_Ex
   196 lemmas [simp del] = ex_simps all_simps split_paired_Ex
   197 declare Let_def [simp]
   197 declare Let_def [simp]
   198 ML_setup {* change_claset (fn cs => cs delSWrapper "split_all_tac") *}
   198 declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *}
   199 
   199 
   200 lemmas exec_rws = executions_def is_exec_frag_def
   200 lemmas exec_rws = executions_def is_exec_frag_def
   201 
   201 
   202 
   202 
   203 
   203