| changeset 2149 | 95aac598a526 |
| parent 2121 | f435d8efd751 |
| child 2326 | b51532dd5689 |
| 2146:a2f70c09e77d | 2149:95aac598a526 |
|---|---|
25 by (induct ts) simp_all |
25 by (induct ts) simp_all |
26 lemmas perm_fixed = perm[simplified perm_fix] |
26 lemmas perm_fixed = perm[simplified perm_fix] |
27 |
27 |
28 ML {* val bl = [[[BEmy 0], [BEmy 0, BEmy 1], [BSet ([(NONE, 0)], [1])]], [[], [BEmy 0, BEmy 1]]] *} |
28 ML {* val bl = [[[BEmy 0], [BEmy 0, BEmy 1], [BSet ([(NONE, 0)], [1])]], [[], [BEmy 0, BEmy 1]]] *} |
29 |
29 |
30 local_setup {* fn ctxt => let val (_, _, ctxt') = define_raw_fv descr sorts [] bl ctxt in ctxt' end *} |
30 local_setup {* fn ctxt => let val (_, _, _, ctxt') = define_raw_fvs descr sorts [] bl ctxt in ctxt' end *} |
31 lemmas fv = fv_rtrm4.simps (*fv_rtrm4_list.simps*) |
31 lemmas fv = fv_rtrm4.simps (*fv_rtrm4_list.simps*) |
32 |
32 |
33 lemma fv_fix: "fv_rtrm4_list = Union o (set o (map fv_rtrm4))" |
33 lemma fv_fix: "fv_rtrm4_list = Union o (set o (map fv_rtrm4))" |
34 by (rule ext) (induct_tac x, simp_all) |
34 by (rule ext) (induct_tac x, simp_all) |
35 lemmas fv_fixed = fv[simplified fv_fix] |
35 lemmas fv_fixed = fv[simplified fv_fix] |