Hello Liliminga, I doubt there can be a full answer to your question unless you provide some more information about what your tactic is doing or how it is implemented.
Generally, this is an indication that the validations constructed by your tactic make use of a reference that is affected by subsequent steps in the proof. When the validations are executed at the end of the proof, the information stored in the reference has changed from what it was when the tactic was executed and therefore the result is different. Hope this helps a bit. Regards, Petros On 28/07/2013 03:17, liliminga wrote: > 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 > -- Petros Papapanagiotou CISA, School of Informatics The University of Edinburgh Email: [email protected] --- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ------------------------------------------------------------------------------ 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
