equal
deleted
inserted
replaced
904 apply (simp (no_asm)) |
904 apply (simp (no_asm)) |
905 apply (frule asm_rl) |
905 apply (frule asm_rl) |
906 apply (drule meta_spec) |
906 apply (drule meta_spec) |
907 apply (erule trans) |
907 apply (erule trans) |
908 apply (drule_tac x = "bin_cat y n a" in meta_spec) |
908 apply (drule_tac x = "bin_cat y n a" in meta_spec) |
909 apply (simp add : bin_cat_assoc_sym min_max.inf_absorb2) |
909 apply (simp add : bin_cat_assoc_sym min.absorb2) |
910 done |
910 done |
911 |
911 |
912 lemma bin_rcat_bl: |
912 lemma bin_rcat_bl: |
913 "(bin_rcat n wl) = bl_to_bin (concat (map (bin_to_bl n) wl))" |
913 "(bin_rcat n wl) = bl_to_bin (concat (map (bin_to_bl n) wl))" |
914 apply (unfold bin_rcat_def) |
914 apply (unfold bin_rcat_def) |