src/HOL/Bali/TypeSafe.thy
changeset 55524 f41ef840f09d
parent 55417 01fbfb60c33e
child 58887 38db8ddc0f57
     1.1 --- a/src/HOL/Bali/TypeSafe.thy	Sun Feb 16 21:33:28 2014 +0100
     1.2 +++ b/src/HOL/Bali/TypeSafe.thy	Sun Feb 16 21:33:28 2014 +0100
     1.3 @@ -3240,10 +3240,10 @@
     1.4                proof -
     1.5                  from normal_s2 conf_args
     1.6                  have "length vs = length pTs"
     1.7 -                  by (simp add: list_all2_def)
     1.8 +                  by (simp add: list_all2_iff)
     1.9                  also from pTs_widen
    1.10                  have "\<dots> = length pTs'"
    1.11 -                  by (simp add: widens_def list_all2_def)
    1.12 +                  by (simp add: widens_def list_all2_iff)
    1.13                  also from wf_dynM
    1.14                  have "\<dots> = length (pars (mthd dynM))"
    1.15                    by (simp add: wf_mdecl_def wf_mhead_def)