| Tue, 03 Mar 2015 16:37:45 +0100 | blanchet | avoid duplicate simp warning for datatypes with explicit products | changeset | files |
| Tue, 03 Mar 2015 16:37:45 +0100 | blanchet | removed needless (and inconsistent) qualifier that messes up with Mirabelle | changeset | files |
| Tue, 03 Mar 2015 16:37:45 +0100 | blanchet | import 'Main' to be on the safe side | changeset | files |
| Sun, 01 Mar 2015 23:35:41 +0100 | wenzelm | added Proof_Context.cterm_of/ctyp_of convenience; | changeset | files |