--- a/src/Doc/Datatypes/Datatypes.thy Tue Jul 15 00:21:32 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Tue Jul 15 00:35:07 2014 +0200
@@ -886,8 +886,9 @@
@{thm list.rel_intros(1)[no_vars]} \\
@{thm list.rel_intros(2)[no_vars]}
-\item[@{text "t."}\hthm{rel_cases} @{text "[consumes 1, case_names t\<^sub>1 \<dots> t\<^sub>m, cases pred]"}\rm:] ~ \\
-@{thm list.rel_cases[no_vars]}
+% FIXME (and add @ before antiquotation below)
+%\item[@{text "t."}\hthm{rel_cases} @{text "[consumes 1, case_names t\<^sub>1 \<dots> t\<^sub>m, cases pred]"}\rm:] ~ \\
+%{thm list.rel_cases[no_vars]}
\end{description}
\end{indentblock}
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Jul 15 00:21:32 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Jul 15 00:35:07 2014 +0200
@@ -1390,7 +1390,7 @@
map2 (fn th => fn 0 => th RS @{thm eq_True[THEN iffD2]} | _ => th)
rel_inject_thms ms;
- val (disc_map_iff_thms, sel_map_thms, sel_set_thms, (rel_cases_thm, rel_cases_attrs)) =
+ val (disc_map_iff_thms, sel_map_thms, sel_set_thms (* FIXME: , (rel_cases_thm, rel_cases_attrs) *)) =
let
val (((Ds, As), Bs), names_lthy) = lthy
|> mk_TFrees (dead_of_bnf fp_bnf)
@@ -1407,6 +1407,7 @@
val selssA = map (map (mk_disc_or_sel ADs)) selss;
val disc_sel_pairs = flat (map2 (map o pair) discsA selssA);
+(* FIXME:
val (rel_cases_thm, rel_cases_attrs) =
let
val rel = mk_rel_of_bnf Ds As Bs fp_bnf;
@@ -1460,6 +1461,7 @@
in
(thm, [consumes_attr, case_names_attr, cases_pred_attr ""])
end;
+*)
val disc_map_iff_thms =
let
@@ -1583,7 +1585,7 @@
|> Proof_Context.export names_lthy lthy
end;
in
- (disc_map_iff_thms, sel_map_thms, sel_set_thms, (rel_cases_thm, rel_cases_attrs))
+ (disc_map_iff_thms, sel_map_thms, sel_set_thms (* FIXME: , (rel_cases_thm, rel_cases_attrs) *))
end;
val anonymous_notes =
@@ -1594,7 +1596,7 @@
val notes =
[(disc_map_iffN, disc_map_iff_thms, simp_attrs),
(mapN, map_thms, code_nitpicksimp_attrs @ simp_attrs),
- (rel_casesN, [rel_cases_thm], rel_cases_attrs),
+(* FIXME: (rel_casesN, [rel_cases_thm], rel_cases_attrs), *)
(rel_distinctN, rel_distinct_thms, simp_attrs),
(rel_injectN, rel_inject_thms, simp_attrs),
(rel_introsN, rel_intro_thms, []),
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Jul 15 00:21:32 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Jul 15 00:35:07 2014 +0200
@@ -127,12 +127,12 @@
fun mk_disc_map_iff_tac ctxt ct exhaust discs maps =
TRYALL Goal.conjunction_tac THEN
- ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
- REPEAT_DETERM o hyp_subst_tac ctxt) THEN
- unfold_thms_tac ctxt maps THEN
- unfold_thms_tac ctxt (map (fn thm => thm RS eqFalseI
- handle THM _ => thm RS eqTrueI) discs) THEN
- ALLGOALS (rtac refl ORELSE' rtac TrueI);
+ ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
+ REPEAT_DETERM o hyp_subst_tac ctxt) THEN
+ unfold_thms_tac ctxt maps THEN
+ unfold_thms_tac ctxt (map (fn thm => thm RS eqFalseI
+ handle THM _ => thm RS eqTrueI) discs) THEN
+ ALLGOALS (rtac refl ORELSE' rtac TrueI);
fun solve_prem_prem_tac ctxt =
REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
@@ -225,7 +225,7 @@
REPEAT_DETERM o (dtac @{thm meta_mp} THEN' rtac refl) THEN' Goal.assume_rule_tac ctxt));
fun mk_rel_coinduct0_tac ctxt dtor_rel_coinduct cts assms exhausts discss selss ctor_defss
- dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses nesting_rel_eqs =
+ dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses nesting_rel_eqs =
rtac dtor_rel_coinduct 1 THEN
EVERY (map11 (fn ct => fn assm => fn exhaust => fn discs => fn sels => fn ctor_defs =>
fn dtor_ctor => fn ctor_inject => fn abs_inject => fn rel_pre_def => fn abs_inverse =>
@@ -278,8 +278,7 @@
@{thms not_True_eq_False not_False_eq_True}) THEN
TRYALL (etac FalseE ORELSE' etac @{thm TrueE}) THEN
unfold_thms_tac ctxt (sels @ sets) THEN
- ALLGOALS (
- REPEAT o (resolve_tac @{thms UnI1 UnI2 imageI} ORELSE'
+ ALLGOALS (REPEAT o (resolve_tac @{thms UnI1 UnI2 imageI} ORELSE'
eresolve_tac @{thms UN_I UN_I[rotated] imageE} ORELSE'
hyp_subst_tac ctxt) THEN'
(rtac @{thm singletonI} ORELSE' atac));