Hi,
I tried to prove a goal by a tactic developed by myself, and all of the
subgoals were done. However the form of “Initial goal proved” returned by HOL4
was different from my original goal’s.
What is the cause of the phenomenon?
Regard,
liliminga
------------------------------------------------------------------------------
See everything from the browser to the database with AppDynamics
Get end-to-end visibility with application monitoring from AppDynamics
Isolate bottlenecks and diagnose root cause in seconds.
Start your free trial of AppDynamics Pro today!
http://pubads.g.doubleclick.net/gampad/clk?id=48808831&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
