# HG changeset patch
# User huffman
# Date 1118190508 -7200
# Node ID 7cd7d21975ad4c6b7ad65856812ac04e89dd1e9d
# Parent  ef32a42f40791f264399230afa71c321b96cb183
fix usage of inverts lemma, which has fewer premises now

diff -r ef32a42f4079 -r 7cd7d21975ad src/HOLCF/ex/Dnat.thy
--- a/src/HOLCF/ex/Dnat.thy	Wed Jun 08 02:27:19 2005 +0200
+++ b/src/HOLCF/ex/Dnat.thy	Wed Jun 08 02:28:28 2005 +0200
@@ -69,7 +69,7 @@
    apply (erule disjE)
     apply (tactic "contr_tac 1")
    apply simp
-  apply (erule (2) dnat.inverts)
+  apply (erule (1) dnat.inverts)
   done
 
 end