2011/10/11 Jonathan von Schroeder <[email protected]>: > Hi all, > im currently having a problem figuring out the meaning of the following > theorem (from realax.ml): >> >> # real_neg;; >> val it : thm = >> |- --x1 = mk_real (\u. ?x1. treal_neg x1 treal_eq u /\ dest_real x1 x1)
You can also look at the version automatically translated to Isabelle by HOL/Import. In the isabelle source the file: src/HOL/Import/HOLLight/HOLLight.thy You can find the following: definition real_neg :: "hollight.real => hollight.real" where "real_neg == %x1. mk_real (%u. EX x1a. treal_eq (treal_neg x1a) u & dest_real x1 x1a)" In the above, the name of the other variable has been automatically changed from 'x1' to 'x1a' to avoid the name clash. Cezary ------------------------------------------------------------------------------ All the data continuously generated in your IT infrastructure contains a definitive record of customers, application performance, security threats, fraudulent activity and more. Splunk takes this data and makes sense of it. Business sense. IT sense. Common sense. http://p.sf.net/sfu/splunk-d2d-oct _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
