equal
deleted
inserted
replaced
28 thm foo.permute_bn |
28 thm foo.permute_bn |
29 thm foo.perm_bn_alpha |
29 thm foo.perm_bn_alpha |
30 thm foo.perm_bn_simps |
30 thm foo.perm_bn_simps |
31 thm foo.bn_finite |
31 thm foo.bn_finite |
32 |
32 |
|
33 |
33 thm foo.distinct |
34 thm foo.distinct |
34 thm foo.induct |
35 thm foo.induct |
35 thm foo.inducts |
36 thm foo.inducts |
36 thm foo.exhaust |
37 thm foo.exhaust |
37 thm foo.fv_defs |
38 thm foo.fv_defs |
43 thm foo.supports |
44 thm foo.supports |
44 thm foo.fsupp |
45 thm foo.fsupp |
45 thm foo.supp |
46 thm foo.supp |
46 thm foo.fresh |
47 thm foo.fresh |
47 |
48 |
48 text {* |
49 |
49 tests by cu |
50 |
50 *} |
51 |
51 |
|
52 |
|
53 text {* *} |
|
54 |
52 |
55 |
53 |
56 (* |
54 (* |
57 thm at_set_avoiding1[THEN exE] |
55 thm at_set_avoiding1[THEN exE] |
58 |
56 |
68 apply(rule Abs_rename_list[THEN exE]) |
66 apply(rule Abs_rename_list[THEN exE]) |
69 apply(simp only: set_eqvt) |
67 apply(simp only: set_eqvt) |
70 apply |
68 apply |
71 sorry |
69 sorry |
72 *) |
70 *) |
|
71 |
|
72 thm foo.exhaust |
|
73 |
|
74 ML {* |
|
75 fun strip_prems_concl trm = |
|
76 (Logic.strip_imp_prems trm, Logic.strip_imp_concl trm) |
|
77 *} |
|
78 |
|
79 |
|
80 ML {* |
|
81 @{thms foo.exhaust} |
|
82 |> map prop_of |
|
83 |> map strip_prems_concl |
|
84 |> map fst |
|
85 |> map (map (Syntax.string_of_term @{context})) |
|
86 |> map cat_lines |
|
87 |> cat_lines |
|
88 |> writeln |
|
89 *} |
73 |
90 |
74 lemma test6: |
91 lemma test6: |
75 fixes c::"'a::fs" |
92 fixes c::"'a::fs" |
76 assumes "\<exists>name. y = Var name \<Longrightarrow> P" |
93 assumes "\<exists>name. y = Var name \<Longrightarrow> P" |
77 and "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
94 and "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |