src/HOL/MicroJava/J/TypeRel.thy
changeset 45231 d85a2fdc586c
parent 44035 322d1657c40c
child 45970 b6d0cff57d96
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Fri Oct 21 11:17:12 2011 +0200
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Fri Oct 21 11:17:14 2011 +0200
     1.3 @@ -97,7 +97,7 @@
     1.4    [inductify]
     1.5    subcls'
     1.6  .
     1.7 -lemma subcls_conv_subcls' [code_inline]:
     1.8 +lemma subcls_conv_subcls' [code_unfold]:
     1.9    "(subcls1 G)^* = (\<lambda>(C, D). subcls' G C D)"
    1.10  by(simp add: subcls'_def subcls1_def rtrancl_def)(simp add: Collect_def)
    1.11