fixed clash with new 'abs' const;
authorwenzelm
Sat, 06 May 2000 00:46:13 +0200
changeset 8820 a1297de19ec7
parent 8819 d04923e183c7
child 8821 b5c3aec69462
fixed clash with new 'abs' const;
src/HOLCF/Cfun3.ML
--- a/src/HOLCF/Cfun3.ML	Fri May 05 22:37:04 2000 +0200
+++ b/src/HOLCF/Cfun3.ML	Sat May 06 00:46:13 2000 +0200
@@ -410,13 +410,13 @@
 
 
 qed_goal "isorep_defined" thy 
-        "[|!x. rep`(abs`x)=x;!y. abs`(rep`y)=y; z~=UU|] ==> rep`z ~= UU"
+        "[|!x. rep`(ab`x)=x;!y. ab`(rep`y)=y; z~=UU|] ==> rep`z ~= UU"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (etac swap 1),
         (dtac notnotD 1),
-        (dres_inst_tac [("f","abs")] cfun_arg_cong 1),
+        (dres_inst_tac [("f","ab")] cfun_arg_cong 1),
         (etac box_equals 1),
         (fast_tac HOL_cs 1),
         (etac (iso_strict RS conjunct1) 1),
@@ -424,7 +424,7 @@
         ]);
 
 qed_goal "isoabs_defined" thy 
-        "[|!x. rep`(abs`x) = x;!y. abs`(rep`y)=y ; z~=UU|] ==> abs`z ~= UU"
+        "[|!x. rep`(ab`x) = x;!y. ab`(rep`y)=y ; z~=UU|] ==> ab`z ~= UU"
  (fn prems =>
         [
         (cut_facts_tac prems 1),