src/HOLCF/Tools/Domain/domain_theorems.ML
 changeset 35512 d1ef88d7de5a parent 35497 979706bd5c16 child 35514 a2cfa413eaab
```     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Mar 02 04:53:18 2010 -0800
1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Mar 02 09:54:50 2010 -0800
1.3 @@ -95,10 +95,6 @@
1.4    InductTacs.case_tac ctxt (v^"=UU") i THEN
1.5    asm_simp_tac (HOLCF_ss addsimps rews) i;
1.6
1.7 -val chain_tac =
1.8 -  REPEAT_DETERM o resolve_tac
1.9 -    [chain_iterate, ch2ch_Rep_CFunR, ch2ch_Rep_CFunL, ch2ch_fst, ch2ch_snd];
1.10 -
1.11  (* ----- general proofs ----------------------------------------------------- *)
1.12
1.13  val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp}
1.14 @@ -171,8 +167,6 @@
1.15
1.16  val pg = pg' thy;
1.17
1.18 -val dc_copy = %%:(dname^"_copy");
1.19 -
1.20  val abs_strict = ax_rep_iso RS (allI RS retraction_strict);
1.21  val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
1.22  val iso_rews = map Drule.export_without_context [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict];
1.23 @@ -195,10 +189,6 @@
1.24            else (%# arg);
1.25        val lhs = (dc_take dname \$ (%%:"Suc" \$ %:"n"))`(con_app con args);
1.26        val rhs = con_app2 con one_rhs args;
1.27 -      fun is_rec arg = Datatype_Aux.is_rec_type (dtyp_of arg);
1.28 -      fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg);
1.29 -      fun nonlazy_rec args = map vname (filter is_nonlazy_rec args);
1.30 -      val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
1.31        val goal = mk_trp (lhs === rhs);
1.32        val rules = [ax_take_Suc, ax_abs_iso, @{thm cfcomp2}];
1.33        val rules2 = @{thms take_con_rules ID1} @ axs_take_strict;
```