1.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Sat Apr 11 08:44:41 2009 -0700
     1.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Mon Apr 13 09:29:55 2009 -0700
     1.3 @@ -288,8 +288,7 @@
     1.4  
     1.5  lemma Cons_not_UU: "a>>s ~= UU"
     1.6  apply (subst Consq_def2)
     1.7 -apply (rule seq.con_rews)
     1.8 -apply (rule Def_not_UU)
     1.9 +apply simp
    1.10  done
    1.11  
    1.12  

     2.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML	Sat Apr 11 08:44:41 2009 -0700
     2.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Mon Apr 13 09:29:55 2009 -0700
     2.3 @@ -387,12 +387,14 @@
     2.4  
     2.5    fun con_defin (con, args) =
     2.6      let
     2.7 -      val concl = mk_trp (defined (con_app con args));
     2.8 -      val goal = lift_defined %: (nonlazy args, concl);
     2.9 -      val rules = @{thms con_defin_rules};
    2.10 -      val tacs = [
    2.11 -        rtac (iso_locale RS iso_abs_defined) 1,
    2.12 -        REPEAT (resolve_tac rules 1 ORELSE assume_tac 1)];
    2.13 +      fun iff_disj (t, []) = HOLogic.mk_not t
    2.14 +        | iff_disj (t, ts) = t === foldr1 HOLogic.mk_disj ts;
    2.15 +      val lhs = con_app con args === UU;
    2.16 +      val rhss = map (fn x => %:x === UU) (nonlazy args);
    2.17 +      val goal = mk_trp (iff_disj (lhs, rhss));
    2.18 +      val rule1 = iso_locale RS @{thm iso.abs_defined_iff};
    2.19 +      val rules = rule1 :: @{thms con_defined_iff_rules};
    2.20 +      val tacs = [simp_tac (HOL_ss addsimps rules) 1];
    2.21      in pg con_appls goal (K tacs) end;
    2.22  in
    2.23    val _ = trace " Proving con_stricts...";

     3.1 --- a/src/HOLCF/ex/Stream.thy	Sat Apr 11 08:44:41 2009 -0700
     3.2 +++ b/src/HOLCF/ex/Stream.thy	Mon Apr 13 09:29:55 2009 -0700
     3.3 @@ -64,10 +64,10 @@
     3.4  section "scons"
     3.5  
     3.6  lemma scons_eq_UU: "(a && s = UU) = (a = UU)"
     3.7 -by (auto, erule contrapos_pp, simp)
     3.8 +by simp
     3.9  
    3.10  lemma scons_not_empty: "[| a && x = UU; a ~= UU |] ==> R"
    3.11 -by auto
    3.12 +by simp
    3.13  
    3.14  lemma stream_exhaust_eq: "(x ~= UU) = (EX a y. a ~= UU &  x = a && y)"
    3.15  by (auto,insert stream.exhaust [of x],auto)
    3.16 @@ -382,7 +382,6 @@
    3.17  
    3.18  lemma slen_scons_eq_rev: "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y |  a = \<bottom> |  #y < Fin (Suc n))"
    3.19   apply (rule stream.casedist [of x], auto)
    3.20 -    apply ((*drule sym,*) drule scons_eq_UU [THEN iffD1],auto)
    3.21     apply (simp add: zero_inat_def)
    3.22    apply (case_tac "#s") apply (simp_all add: iSuc_Fin)
    3.23   apply (case_tac "#s") apply (simp_all add: iSuc_Fin)