Added headers and made various small mods.
(* Title: HOL/IOA/example/Channels.ML
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
Copyright 1994 TU Muenchen
Derived rules
*)
local
val SS = action_ss addsimps
(Channels.srch_asig_def ::
Channels.rsch_asig_def ::
actions_def :: asig_projections @ set_lemmas)
in
val in_srch_asig = prove_goal Channels.thy
"S_msg(m) ~: actions(srch_asig) & \
\ R_msg(m) ~: actions(srch_asig) & \
\ S_pkt(pkt) : actions(srch_asig) & \
\ R_pkt(pkt) : actions(srch_asig) & \
\ S_ack(b) ~: actions(srch_asig) & \
\ R_ack(b) ~: actions(srch_asig) & \
\ C_m_s ~: actions(srch_asig) & \
\ C_m_r ~: actions(srch_asig) & \
\ C_r_s ~: actions(srch_asig) & \
\ C_r_r(m) ~: actions(srch_asig)"
(fn _ => [simp_tac SS 1]);
val in_rsch_asig = prove_goal Channels.thy
"S_msg(m) ~: actions(rsch_asig) & \
\ R_msg(m) ~: actions(rsch_asig) & \
\ S_pkt(pkt) ~: actions(rsch_asig) & \
\ R_pkt(pkt) ~: actions(rsch_asig) & \
\ S_ack(b) : actions(rsch_asig) & \
\ R_ack(b) : actions(rsch_asig) & \
\ C_m_s ~: actions(rsch_asig) & \
\ C_m_r ~: actions(rsch_asig) & \
\ C_r_s ~: actions(rsch_asig) & \
\ C_r_r(m) ~: actions(rsch_asig)"
(fn _ => [simp_tac SS 1]);
end;