Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/MicroJava/BV/JVM.thy
changeset 32960 69916a850301
parent 26450 158b924b5153
child 33639 603320b93668 
--- a/src/HOL/MicroJava/BV/JVM.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/MicroJava/BV/JVM.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MicroJava/BV/JVM.thy
-    ID:         $Id$
     Author:     Tobias Nipkow, Gerwin Klein
     Copyright   2000 TUM
 *)
@@ -37,7 +36,7 @@
   apply (rule is_bcv_kildall)
        apply (simp (no_asm) add: sl_triple_conv [symmetric]) 
        apply (force intro!: semilat_JVM_slI dest: wf_acyclic 
-	 simp add: symmetric sl_triple_conv)
+         simp add: symmetric sl_triple_conv)
       apply (simp (no_asm) add: JVM_le_unfold)
       apply (blast intro!: order_widen wf_converse_subcls1_impl_acc_subtype
                    dest: wf_subcls1 wfP_acyclicP wf_prog_ws_prog)
isabelle