equal
deleted
inserted
replaced
15 lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s" |
15 lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s" |
16 by simp |
16 by simp |
17 |
17 |
18 lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)" |
18 lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)" |
19 by (simp add: comp_def) |
19 by (simp add: comp_def) |
20 |
|
21 lemma meta_iffD2: |
|
22 "\<lbrakk> PROP P \<equiv> PROP Q; PROP Q \<rbrakk> \<Longrightarrow> PROP P" |
|
23 by simp |
|
24 |
20 |
25 lemma o_eq_dest_lhs: |
21 lemma o_eq_dest_lhs: |
26 "a o b = c \<Longrightarrow> a (b v) = c v" |
22 "a o b = c \<Longrightarrow> a (b v) = c v" |
27 by clarsimp |
23 by clarsimp |
28 |
24 |