equal
deleted
inserted
replaced
63 by (auto simp add: cert_def make_cert_def nth_append) |
63 by (auto simp add: cert_def make_cert_def nth_append) |
64 |
64 |
65 |
65 |
66 lemma (in lbv) le_top [simp, intro]: |
66 lemma (in lbv) le_top [simp, intro]: |
67 "x <=_r \<top>" |
67 "x <=_r \<top>" |
68 by (insert top) simp |
68 using top by simp |
69 |
69 |
70 |
70 |
71 lemma (in lbv) merge_mono: |
71 lemma (in lbv) merge_mono: |
72 assumes less: "ss2 \<le>|r| ss1" |
72 assumes less: "ss2 \<le>|r| ss1" |
73 assumes x: "x \<in> A" |
73 assumes x: "x \<in> A" |