# HG changeset patch
# User paulson
# Date 925723091 -7200
# Node ID c09997086ca7e7e410dbbedc66d698aa90357fe0
# Parent  128cf997c768638a88ac598ddf2584df3b024dd0
tidied

diff -r 128cf997c768 -r c09997086ca7 src/HOL/UNITY/SubstAx.ML
--- a/src/HOL/UNITY/SubstAx.ML	Mon May 03 10:57:14 1999 +0200
+++ b/src/HOL/UNITY/SubstAx.ML	Mon May 03 11:18:11 1999 +0200
@@ -397,7 +397,7 @@
 qed "Completion";
 
 
-Goal "[| finite I |] \
+Goal "finite I \
 \     ==> (ALL i:I. F : (A i) LeadsTo (A' i Un C)) -->  \
 \         (ALL i:I. F : (A' i) Co (A' i Un C)) --> \
 \         F : (INT i:I. A i) LeadsTo ((INT i:I. A' i) Un C)";
@@ -406,7 +406,7 @@
 by (Clarify_tac 1);
 by (dtac ball_Constrains_INT 1);
 by (asm_full_simp_tac (simpset() addsimps [Completion]) 1); 
-qed "Finite_completion";
+qed_spec_mp "Finite_completion";
 
 
 (*proves "ensures/leadsTo" properties when the program is specified*)
diff -r 128cf997c768 -r c09997086ca7 src/HOL/UNITY/WFair.ML
--- a/src/HOL/UNITY/WFair.ML	Mon May 03 10:57:14 1999 +0200
+++ b/src/HOL/UNITY/WFair.ML	Mon May 03 11:18:11 1999 +0200
@@ -528,5 +528,5 @@
 by (Clarify_tac 1);
 by (dtac ball_constrains_INT 1);
 by (asm_full_simp_tac (simpset() addsimps [completion]) 1); 
-qed "finite_completion";
+qed_spec_mp "finite_completion";