Hi,
Is there a way to turn off the pretty printing of specialized notation,
while still having the parser recognize it?
For example, what I want to do is prove the equivalency of 2 sets.
(--`{1;2} = {x | (x = 1) \/ (x = 2)}`--)
Can I enter in above term in the interactive prompt, and have the
display show it in it's native term form? So it would look something
like this..
(--`(1 INSERT (2 INSERT EMPTY)) = ???`--))
-Tony
-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2005.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
