src/HOLCF/IOA/meta_theory/Automata.ML

 The I/O automata of Lynch and Tuttle.
 *)
 
 (* Has been removed from HOL-simpset, who knows why? *)
 Addsimps [Let_def];
+Delsimps [split_paired_Ex];
 
 open reachable;
 
 val ioa_projections = [asig_of_def, starts_of_def, trans_of_def,wfair_of_def,sfair_of_def];