src/HOLCF/IOA/Modelcheck/Ring3.ML
author wenzelm
Fri, 20 Aug 1999 16:16:16 +0200
changeset 7310 298b0dcadf2e
parent 7299 743b22579a2f
permissions -rw-r--r--
activate example;


val aut_simps = [Greater_def,one_leader_def,
  one_leader_asig_def,one_leader_trans_def,one_leader_initial_def,
  ring_def,aut0_asig_def,aut0_trans_def,aut0_initial_def,aut0_def,
  aut1_asig_def,aut1_trans_def,aut1_initial_def,aut1_def,
  aut2_asig_def,aut2_trans_def,aut2_initial_def,aut2_def];

(* property to prove: at most one (of 3) members of the ring will
	declare itself to leader *)
Goal "ring =<| one_leader";
by (is_sim_tac aut_simps 1); 
by Auto_tac;
qed"at_most_one_leader";