--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Fri Feb 26 07:17:29 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Fri Feb 26 08:37:03 2010 -0800
@@ -198,6 +198,7 @@
(rep_const, abs_const) (ax_rep_iso, ax_abs_iso) thy;
val axs_con_def = #con_defs result;
+val con_compacts = #con_compacts result;
val sel_rews = #sel_rews result;
(* ----- theorems concerning the isomorphism -------------------------------- *)
@@ -459,22 +460,6 @@
val con_rews = con_stricts @ con_defins;
end;
-local
- val rules =
- [compact_sinl, compact_sinr, compact_spair, compact_up, compact_ONE];
- fun con_compact (con, _, args) =
- let
- val concl = mk_trp (mk_compact (con_app con args));
- val goal = lift (fn x => mk_compact (%#x)) (args, concl);
- val tacs = [
- rtac (iso_locale RS iso_compact_abs) 1,
- REPEAT (resolve_tac rules 1 ORELSE atac 1)];
- in pg con_appls goal (K tacs) end;
-in
- val _ = trace " Proving con_compacts...";
- val con_compacts = map con_compact cons;
-end;
-
val _ = trace " Proving dist_les...";
val dist_les =
let