To make my question more concrete, here's an example.
In arith.ml there is a theorem "LT_LE" which states:
!m n. (m < n) <=> (m <= n) /\ ~(m = n)
Replaying the proof until just before "POP_ASSUM MP_TAC", I get to this
state:
# p();;
val it : goalstack = 1 subgoal (2 total)
0 [`n < n`]
`F`
This looks straightforward, but the goal printer is hiding information:
# snd (List.hd (fst (top_realgoal ())));;
val it : thm = m < n, m = n |- n < n
What do these extra terms mean?
Thanks again,
Jeremy
------------------------------------------------------------------------------
Create and Deploy Rich Internet Apps outside the browser with Adobe(R)AIR(TM)
software. With Adobe AIR, Ajax developers can use existing skills and code to
build responsive, highly engaging applications that combine the power of local
resources and data with the reach of the web. Download the Adobe AIR SDK and
Ajax docs to start building applications today-http://p.sf.net/sfu/adobe-com
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
