diff -r 3a8d722fd3ff -r 16c4ea954511 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";