# HG changeset patch
# User wenzelm
# Date 949404407 -3600
# Node ID a6a4fb7b819b66cf5f12cde10780c662d4ebfe47
# Parent  e59e93ad85eb186318d5693d111328a104a2148f
eliminated nonascii;

diff -r e59e93ad85eb -r a6a4fb7b819b src/HOL/MicroJava/J/WellType.thy
--- a/src/HOL/MicroJava/J/WellType.thy	Mon Jan 31 18:30:35 2000 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy	Tue Feb 01 12:26:47 2000 +0100
@@ -171,7 +171,7 @@
 	nodups pns \\<and>
 	unique lvars \\<and>
 	(\\<forall>pn\\<in>set pns. map_of lvars pn = None) \\<and>
-	(\\<forall>(vn,T)\\<in>set lvars. is_type G T) &
+	(\\<forall>(vn,T)\\<in>set lvars. is_type G T) &
 	(let E = (G,map_of lvars(pns[\\<mapsto>]pTs)(This\\<mapsto>Class C)) in
 	 E\\<turnstile>blk\\<surd> \\<and> (\\<exists>T. E\\<turnstile>res\\<Colon>T \\<and> G\\<turnstile>T\\<preceq>rT))"