src/HOL/Bali/TypeSafe.thy
changeset 18585 5d379fe2eb74
parent 18576 8d98b7711e47
child 19796 d86e7b1fc472
     1.1 --- a/src/HOL/Bali/TypeSafe.thy	Thu Jan 05 22:29:53 2006 +0100
     1.2 +++ b/src/HOL/Bali/TypeSafe.thy	Thu Jan 05 22:29:55 2006 +0100
     1.3 @@ -169,7 +169,7 @@
     1.4  lemma conf_fits: "G,s\<turnstile>v\<Colon>\<preceq>T \<Longrightarrow> G,s\<turnstile>v fits T"
     1.5  apply (unfold fits_def)
     1.6  apply clarify
     1.7 -apply (erule swap, simp (no_asm_use))
     1.8 +apply (erule contrapos_np, simp (no_asm_use))
     1.9  apply (drule conf_RefTD)
    1.10  apply auto
    1.11  done