# HG changeset patch
# User oheimb
# Date 890750972 -3600
# Node ID 6fbd9838ccae9b3e43356910ce1162f216b7387d
# Parent  f83cd6a06676a0101474cd10e6a2370cb9ba098f
added finite_acyclic_wf_converse: corrected 8bit chars

diff -r f83cd6a06676 -r 6fbd9838ccae src/HOL/WF_Rel.ML
--- a/src/HOL/WF_Rel.ML	Tue Mar 24 15:46:34 1998 +0100
+++ b/src/HOL/WF_Rel.ML	Tue Mar 24 15:49:32 1998 +0100
@@ -118,7 +118,7 @@
 qed_spec_mp "finite_acyclic_wf";
 
 qed_goal "finite_acyclic_wf_converse" thy 
- "ÄX. Ëfinite r; acyclic rÌ êë wf (r^-1)" (K [
+ "!!X. [|finite r; acyclic r|] ==> wf (r^-1)" (K [
 	etac (finite_converse RS iffD2 RS finite_acyclic_wf) 1,
 	etac (acyclic_converse RS iffD2) 1]);