--- a/IOA/example/Channels.ML Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-(* 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;