equal
deleted
inserted
replaced
2867 apply(drule_tac x="x" in meta_spec) |
2867 apply(drule_tac x="x" in meta_spec) |
2868 apply(auto simp add: ty.inject) |
2868 apply(auto simp add: ty.inject) |
2869 apply(rotate_tac 10) |
2869 apply(rotate_tac 10) |
2870 apply(drule_tac x="a" in meta_spec) |
2870 apply(drule_tac x="a" in meta_spec) |
2871 apply(auto simp add: ty.inject) |
2871 apply(auto simp add: ty.inject) |
2872 apply(blast) |
|
2873 apply(blast) |
|
2874 apply(blast) |
|
2875 apply(rotate_tac 10) |
2872 apply(rotate_tac 10) |
2876 apply(drule_tac x="a" in meta_spec) |
2873 apply(drule_tac x="a" in meta_spec) |
2877 apply(auto simp add: ty.inject) |
2874 apply(auto simp add: ty.inject) |
2878 apply(blast) |
|
2879 apply(blast) |
|
2880 apply(blast) |
|
2881 done |
2875 done |
2882 |
2876 |
2883 termination |
2877 termination |
2884 apply(relation "measure (case_sum (size\<circ>fst) (size\<circ>fst))") |
2878 apply(relation "measure (case_sum (size\<circ>fst) (size\<circ>fst))") |
2885 apply(simp_all) |
2879 apply(simp_all) |