| changeset 55062 | 6d3fad6f01c9 |
| parent 55059 | ef2e0fb783c6 |
| child 55066 | 4e5ddf3162ac |
| 55061:a0adf838e2d1 | 55062:6d3fad6f01c9 |
|---|---|
155 |
155 |
156 (*FIXME: duplicates lemma from Record.thy*) |
156 (*FIXME: duplicates lemma from Record.thy*) |
157 lemma o_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v" |
157 lemma o_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v" |
158 by clarsimp |
158 by clarsimp |
159 |
159 |
160 ML_file "Tools/bnf_def_tactics.ML" |
160 ML_file "Tools/BNF/bnf_def_tactics.ML" |
161 ML_file "Tools/bnf_def.ML" |
161 ML_file "Tools/BNF/bnf_def.ML" |
162 |
162 |
163 end |
163 end |