diff -r bac0d673b6d6 -r a90fe83f58ea src/HOL/Bali/Example.thy --- a/src/HOL/Bali/Example.thy Fri May 15 10:01:57 2009 +0200 +++ b/src/HOL/Bali/Example.thy Sat May 16 11:28:02 2009 +0200 @@ -1075,10 +1075,7 @@ lemma max_spec_Base_foo: "max_spec tprg S (ClassT Base) \name=foo,parTs=[NT]\ = {((ClassT Base, \access=Public,static=False,pars=[z],resT=Class Base\) , [Class Base])}" -apply (unfold max_spec_def) -apply (simp (no_asm) add: appl_methds_Base_foo) -apply auto -done +by (simp (no_asm) add: max_spec_def appl_methds_Base_foo) section "well-typedness"