In the middle of an interactive proof with lots of abbreviations to prevent
unmanageably large terms, I might at some point want to prove something by
expanding all the abbreviations.
For example, `HD ls` might be obvious when you unabbreviate ls (and all
abbreviations inside it), since it is ultimately a known CONS. It may,
however, be a CONS of a large term.
The only way I know how to do this is to write the term out by hand and
prove it as a subgoal:
`HD ls = blah blah blah blah blah blah blah` by (unabbrev_all_tac >> rw[])
How can I get that without manually typing out all the blahs?
------------------------------------------------------------------------------
Monitor your physical, virtual and cloud infrastructure from a single
web console. Get in-depth insight into apps, servers, databases, vmware,
SAP, cloud infrastructure, etc. Download 30-day Free Trial.
Pricing starts from $795 for 25 servers or applications!
http://p.sf.net/sfu/zoho_dev2dev_nov
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
