src/HOLCF/domain/theorems.ML
changeset 3323 194ae2e0c193
parent 3044 3e3087aa69e7
child 4008 2444085532c6
     1.1 --- a/src/HOLCF/domain/theorems.ML	Fri May 23 18:55:28 1997 +0200
     1.2 +++ b/src/HOLCF/domain/theorems.ML	Sun May 25 11:07:52 1997 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4                                  cut_facts_tac prems 1,
     1.5                                  fast_tac HOL_cs 1]);
     1.6  
     1.7 -val dist_eqI = prove_goal Porder.thy "~ x << y ==> x ~= y" (fn prems => [
     1.8 +val dist_eqI = prove_goal Porder.thy "~(x::'a::po) << y ==> x ~= y" (fn prems => [
     1.9                                  rtac rev_contrapos 1,
    1.10                                  etac (antisym_less_inverse RS conjunct1) 1,
    1.11                                  resolve_tac prems 1]);