changeset 31197 | c1c163ec6c44 |
parent 31166 | a90fe83f58ea |
child 32456 | 341c83339aeb |
--- a/src/HOL/Bali/Example.thy Mon May 18 09:48:06 2009 +0200 +++ b/src/HOL/Bali/Example.thy Mon May 18 23:15:38 2009 +0200 @@ -1075,7 +1075,7 @@ lemma max_spec_Base_foo: "max_spec tprg S (ClassT Base) \<lparr>name=foo,parTs=[NT]\<rparr> = {((ClassT Base, \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>) , [Class Base])}" -by (simp (no_asm) add: max_spec_def appl_methds_Base_foo) +by (simp add: max_spec_def appl_methds_Base_foo Collect_conv_if) section "well-typedness"