--- a/src/HOLCF/IOA/NTP/Impl.ML Mon Jun 22 17:12:27 1998 +0200
+++ b/src/HOLCF/IOA/NTP/Impl.ML Mon Jun 22 17:13:09 1998 +0200
@@ -28,7 +28,7 @@
in_rsch_asig];
Addcongs [let_weak_cong];
-goal Impl.thy
+Goal
"fst(x) = sen(x) & \
\ fst(snd(x)) = rec(x) & \
\ fst(snd(snd(x))) = srch(x) & \
@@ -37,7 +37,7 @@
[sen_def,rec_def,srch_def,rsch_def]) 1);
Addsimps [result()];
-goal Impl.thy "a:actions(sender_asig) \
+Goal "a:actions(sender_asig) \
\ | a:actions(receiver_asig) \
\ | a:actions(srch_asig) \
\ | a:actions(rsch_asig)";
@@ -67,7 +67,7 @@
(* INVARIANT 1 *)
-goalw Impl.thy impl_ioas "invariant impl_ioa inv1";
+Goalw impl_ioas "invariant impl_ioa inv1";
by (rtac invariantI 1);
by (asm_full_simp_tac (simpset()
addsimps [inv1_def, hdr_sum_def, Sender.srcvd_def,
@@ -150,7 +150,7 @@
(* INVARIANT 2 *)
- goal Impl.thy "invariant impl_ioa inv2";
+Goal "invariant impl_ioa inv2";
by (rtac invariantI1 1);
(* Base case *)
@@ -212,7 +212,7 @@
(* INVARIANT 3 *)
-goal Impl.thy "invariant impl_ioa inv3";
+Goal "invariant impl_ioa inv3";
by (rtac invariantI 1);
(* Base case *)
@@ -278,7 +278,7 @@
(* INVARIANT 4 *)
-goal Impl.thy "invariant impl_ioa inv4";
+Goal "invariant impl_ioa inv4";
by (rtac invariantI 1);
(* Base case *)