equal
deleted
inserted
replaced
906 "\<lbrakk> check_type cG mxs mxr (OK (Some (ST, LT))); length ST \<le> mxs\<rbrakk> |
906 "\<lbrakk> check_type cG mxs mxr (OK (Some (ST, LT))); length ST \<le> mxs\<rbrakk> |
907 \<Longrightarrow>check_type cG (length ST) mxr (OK (Some (ST, LT)))" |
907 \<Longrightarrow>check_type cG (length ST) mxr (OK (Some (ST, LT)))" |
908 by (simp add: check_type_def states_lower) |
908 by (simp add: check_type_def states_lower) |
909 |
909 |
910 lemma max_same_iter [simp]: "max (x::'a::linorder) (max x y) = max x y" |
910 lemma max_same_iter [simp]: "max (x::'a::linorder) (max x y) = max x y" |
911 by (simp del: max_assoc add: max_assoc [THEN sym]) |
911 by (simp add: AC_max.assoc [THEN sym]) |
912 |
912 |
913 (* ******************************************************************* *) |
913 (* ******************************************************************* *) |
914 |
914 |
915 constdefs |
915 constdefs |
916 bc_mt_corresp :: " |
916 bc_mt_corresp :: " |