IOA/example/Impl.ML

--- a/IOA/example/Impl.ML	Fri Nov 11 10:35:03 1994 +0100
+++ b/IOA/example/Impl.ML	Mon Nov 21 17:50:34 1994 +0100
@@ -47,7 +47,7 @@
 (* Instantiation of a tautology? *)
 goal Packet.thy "!x. x = packet --> hdr(x) = hdr(packet)";
  by (simp_tac (HOL_ss addsimps [Packet.hdr_def]) 1);
-val eq_packet_imp_eq_hdr = result();
+qed "eq_packet_imp_eq_hdr";
 
 
 (* INVARIANT 1 *)
@@ -124,7 +124,7 @@
 
 by (EVERY1[tac, tac, tac, tac, tac, tac]);
 
-val inv1 = result();
+qed "inv1";
 
 
 
@@ -197,7 +197,7 @@
   by (dres_inst_tac [("k","hdr_sum(srch(s), sbit(sen(s)))")] 
                      (standard(leq_add_leq RS mp)) 1);
   by (asm_full_simp_tac HOL_ss 1);
-val inv2 = result();
+qed "inv2";
 
 
 (* INVARIANT 3 *)
@@ -297,7 +297,7 @@
   by (dtac mp 1);
   by (assume_tac 1);
   by (assume_tac 1);
-val inv3 = result();
+qed "inv3";
 
 
 
@@ -380,7 +380,7 @@
   by (dtac (left_add_leq RS mp) 1);
   by (asm_full_simp_tac list_ss 1);
   by (asm_full_simp_tac arith_ss 1);
-val inv4 = result();
+qed "inv4";