src/HOL/MicroJava/BV/BVExample.thy
changeset 31998 2c7a24f74db9
parent 31867 4d278bbb5cc8
child 33954 1bc3b688548c
     1.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Tue Jul 14 10:53:44 2009 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Tue Jul 14 10:54:04 2009 +0200
     1.3 @@ -467,7 +467,7 @@
     1.4  
     1.5  lemmas [code] = JType.sup_def [unfolded exec_lub_def] JVM_le_unfold
     1.6  
     1.7 -lemmas [code ind] = rtranclp.rtrancl_refl converse_rtranclp_into_rtranclp
     1.8 +lemmas [code_ind] = rtranclp.rtrancl_refl converse_rtranclp_into_rtranclp
     1.9  
    1.10  code_module BV
    1.11  contains