Hi, I am fairly new to HOL Light and OCaml. I'm unable to find a proof for
Pierce's law in HOL Light. Could you provide me with a proof for it?
Also, I was trying to prove a simple goal
# g `!p q r. p \/ (q /\ r) ==> p /\ q \/ p /\ r`;;
# e (INTRO_TAC "!p q r; p | q r");;
but I keep getting the error 'Unbound value INTRO_TAC"
I would really appreciate it if someone could clarify my doubts. Looking
forward to your response eagerly.
Thanks and Regards
Shruti
------------------------------------------------------------------------------
Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server
from Actuate! Instantly Supercharge Your Business Reports and Dashboards
with Interactivity, Sharing, Native Excel Exports, App Integration & more
Get technology previously reserved for billion-dollar corporations, FREE
http://pubads.g.doubleclick.net/gampad/clk?id=157005751&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
