diff -r 414a68d72279 -r 1fa4725c4656 src/HOL/MicroJava/DFA/Kildall.thy --- a/src/HOL/MicroJava/DFA/Kildall.thy Thu Jan 13 21:50:13 2011 +0100 +++ b/src/HOL/MicroJava/DFA/Kildall.thy Thu Jan 13 23:50:16 2011 +0100 @@ -172,7 +172,7 @@ done } note this [dest] - from prems show ?thesis by blast + from assms show ?thesis by blast qed