Hey guys,
I am learning to use HOL. When I use METIS_TAC, I don't know the system's
response.
For example:
what I input are:
-open arithmeticTheory;
-val divides_def = Define `divides a b = ?x. b = a * x`;
-set_fixity "divides" (Infix(NONASSOC,450));
-g`!x.x divides 0`;
-e(METIS_TAC [divides_def,MULT_CLAUSES]);
Finally,what system response is:
OK..
metis: r[+0+10]+0+0+0+1+2#
> val it =
Initial goal proved.
|- !x. x divides 0 : proof
* Does anyone know what is the meaning of metis: r[+0+10]+0+0+0+1+2# ?
Thanks! --Wish.------------------------------------------------------------------------------
BPM Camp - Free Virtual Workshop May 6th at 10am PDT/1PM EDT
Develop your own process in accordance with the BPMN 2 standard
Learn Process modeling best practices with Bonita BPM through live exercises
http://www.bonitasoft.com/be-part-of-it/events/bpm-camp-virtual- event?utm_
source=Sourceforge_BPM_Camp_5_6_15&utm_medium=email&utm_campaign=VA_SF
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
