Freek, can you assure me this is not a bug (it works), ending a miz3 proof with
a semicolon:
angle F O' D <_ang angle C O A [H3'] by H3, AngleSymmetry_THM;
seg F D <__ seg C A by H1', H2, H3', H4, EuclidPropositionI_24Help;
qed by -, SegmentSymmetry_THM;
end;
`;;
You suggested that I might prefer that (I do, as it simplifies your syntax),
and I accidentally learned that miz3 accepts it. But if you think it's a bug,
I'll stop doing it :)
--
Best,
Bill
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
