diff -r 37a6e2f55230 -r 44ff2275d44f IOA/example/Channels.ML --- a/IOA/example/Channels.ML Wed Nov 09 19:50:36 1994 +0100 +++ b/IOA/example/Channels.ML Wed Nov 09 19:51:09 1994 +0100 @@ -1,10 +1,19 @@ +(* 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_def :: set_lemmas) + actions_def :: asig_projections @ set_lemmas) in -val _ = goal Channels.thy + +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) & \ @@ -14,13 +23,10 @@ \ 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)"; - -val _ = by (simp_tac SS 1); + \ C_r_r(m) ~: actions(srch_asig)" + (fn _ => [simp_tac SS 1]); -val in_srch_asig = result(); - -val _ = goal Channels.thy +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) & \ @@ -30,10 +36,7 @@ \ 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)"; - -val _ = by (simp_tac SS 1); - -val in_rsch_asig = result(); + \ C_r_r(m) ~: actions(rsch_asig)" + (fn _ => [simp_tac SS 1]); end;