Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: Wishnu Prasetya <wishnu@nl.ruu.cs>
Message-Id: <199212150903.AA20712@infix.cs.ruu.nl>
Subject: HELP: deleting assumption.
To: info-hol@edu.uidaho.cs.ted (hol mailing list)
Date: Tue, 15 Dec 92 10:03:46 MET
Cc: wishnu@nl.ruu.cs (Wishnu Prasetya)

Sometimes tactics such as resolutions generate too many assumption,
and one may wish to eliminate those which are really superflous. Is
there any standard tactic that can do this? I have search in manual
but found nothing so far. Did I miss something?

Another problem that I have is this:

   let NO_EFFECT_TAC p = EVERY_ASSUM
       (\thm. (let hyp = snd(dest_thm thm) in
              let q = fst(dest_comb hyp) in
              let r="^p=^q" in
              ALL_TAC) ? ALL_TAC) ;;

   #set_goal(["(f:bool->bool) x"], "y:bool") ;;
   "y"
       [ "f x " ] 

   () : void

   #e (NO_EFFECT_TAC "x:bool") ;;
   OK..
   Badly typed application of:  "$= x"
      which has type:           ":bool -> bool"
   to the argument term:        "f"
      which has type:           ":bool -> bool"

   "y"
       [ "x ==> y" ]
       [ "f x" ]

   () : void

NO_EFFECT_TAC "x:bool" results the intended effect on the goal, namely
nothing. But I don't understand why it complains about bad type
application. I have put the '?' trapping in case of failure. Yet the
error message is generated, and yet the error is not relevant since it
has no effect to the result.

My thanks in advance for any hint from you.

-Wishnu Prasetya-

 --