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;