src/HOLCF/domain/theorems.ML
changeset 1644 681f70ca3cf7
parent 1638 69c094639823
child 1674 33aff4d854e4
     1.1 --- a/src/HOLCF/domain/theorems.ML	Thu Apr 04 12:58:47 1996 +0200
     1.2 +++ b/src/HOLCF/domain/theorems.ML	Thu Apr 04 13:28:50 1996 +0200
     1.3 @@ -56,10 +56,11 @@
     1.4  (* ----- general proofs ----------------------------------------------------- *)
     1.5  
     1.6  val quant_ss = HOL_ss addsimps (map (fn s => prove_goal HOL.thy s (fn _ =>[
     1.7 -		fast_tac HOL_cs 1]))["(x. P x  Q)=((x. P x)  Q)",
     1.8 -			    	     "(x. P  Q x) = (P  (x. Q x))"]);
     1.9 +		fast_tac HOL_cs 1]))["(!x. P x & Q)=((!x. P x) & Q)",
    1.10 +			    	     "(!x. P & Q x) = (P & (!x. Q x))"]);
    1.11  
    1.12 -val all2E = prove_goal HOL.thy " x y . P x y; P x y  R   R" (fn prems =>[
    1.13 +val all2E = prove_goal HOL.thy "[| !x y . P x y; P x y ==> R |] ==> R"
    1.14 + (fn prems =>[
    1.15  				resolve_tac prems 1,
    1.16  				cut_facts_tac prems 1,
    1.17  				fast_tac HOL_cs 1]);
    1.18 @@ -70,13 +71,13 @@
    1.19                                  dtac notnotD 1,
    1.20  				etac (hd prems) 1]);
    1.21  
    1.22 -val dist_eqI = prove_goal Porder.thy " x  y  x  y" (fn prems => [
    1.23 +val dist_eqI = prove_goal Porder.thy "~ x << y ==> x ~= y" (fn prems => [
    1.24                                  rtac swap3 1,
    1.25  				etac (antisym_less_inverse RS conjunct1) 1,
    1.26  				resolve_tac prems 1]);
    1.27 -val cfst_strict  = prove_goal Cprod3.thy "cfst` = " (fn _ => [
    1.28 +val cfst_strict  = prove_goal Cprod3.thy "cfst`UU = UU" (fn _ => [
    1.29  			(simp_tac (HOLCF_ss addsimps [inst_cprod_pcpo2]) 1)]);
    1.30 -val csnd_strict  = prove_goal Cprod3.thy "csnd` = " (fn _ => [
    1.31 +val csnd_strict  = prove_goal Cprod3.thy "csnd`UU = UU" (fn _ => [
    1.32  			(simp_tac (HOLCF_ss addsimps [inst_cprod_pcpo2]) 1)]);
    1.33  
    1.34  in