| Wed, 15 Dec 2010 19:15:06 -0800 | huffman | add notsqsubseteq syntax | changeset | files |
| Wed, 15 Dec 2010 20:52:20 +0100 | wenzelm | show: display goal refinement rule as "state", to avoid odd Output.urgent_message and make its association with the goal more explicit; | changeset | files |
| Wed, 15 Dec 2010 19:41:24 +0100 | blanchet | make sure errors generated in a thread don't vanish in cyberspace (e.g., when invoking Sledgehammer with unknown facts) | changeset | files |