[Hol-checkins] CVS: hol98/src/boss bossLib.sig,1.25,1.26 bossLib.sml,1.58,1.59

[Konrad S. <sl...@us...>]

Update of /cvsroot/hol/hol98/src/boss
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv24572

Modified Files:
	bossLib.sig bossLib.sml 
Log Message:
Finally added METIS_TAC and METIS_PROVE to bossLib. Consequently,
they will be available by default. 



Index: bossLib.sig
===================================================================
RCS file: /cvsroot/hol/hol98/src/boss/bossLib.sig,v
retrieving revision 1.25
retrieving revision 1.26
diff -b -C2 -d -r1.25 -r1.26
*** bossLib.sig	2 Jul 2003 02:00:47 -0000	1.25
--- bossLib.sig	26 Mar 2005 10:21:30 -0000	1.26
***************
*** 28,33 ****
--- 28,35 ----
  
    val PROVE          : thm list -> term -> thm   (* First order *)
+   val METIS_PROVE    : thm list -> term -> thm   (* First order *)
    val DECIDE         : term -> thm               (* Cooperating dec. procs *)
    val PROVE_TAC      : thm list -> tactic
+   val METIS_TAC      : thm list -> tactic
    val DECIDE_TAC     : tactic
  

Index: bossLib.sml
===================================================================
RCS file: /cvsroot/hol/hol98/src/boss/bossLib.sml,v
retrieving revision 1.58
retrieving revision 1.59
diff -b -C2 -d -r1.58 -r1.59
*** bossLib.sml	5 Aug 2004 04:39:13 -0000	1.58
--- bossLib.sml	26 Mar 2005 10:21:30 -0000	1.59
***************
*** 55,58 ****
--- 55,60 ----
  val PROVE          = BasicProvers.PROVE
  val PROVE_TAC      = BasicProvers.PROVE_TAC
+ val METIS_PROVE    = BasicProvers.PROVE
+ val METIS_TAC      = BasicProvers.PROVE_TAC
  val RW_TAC         = BasicProvers.RW_TAC
  val SRW_TAC        = BasicProvers.SRW_TAC