| Fri, 25 Nov 2011 10:52:30 +0100 | bulwahn | improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory | changeset | files |
| Fri, 25 Nov 2011 00:18:59 +0000 | Christian Urban | in a local context, also the free variable case needs to be analysed default tip | changeset | files |
| Thu, 24 Nov 2011 21:41:58 +0100 | wenzelm | speed-up proof; | changeset | files |
| Thu, 24 Nov 2011 21:15:20 +0100 | wenzelm | more abstract datatype stamp, which avoids pointless allocation of mutable cells; | changeset | files |
| Thu, 24 Nov 2011 21:01:06 +0100 | wenzelm | modernized some old-style infix operations, which were left over from the time of ML proof scripts; | changeset | files |
| Thu, 24 Nov 2011 20:45:34 +0100 | wenzelm | simplified -- empty_ss already contains minimal mksimps; | changeset | files |