| Sun, 26 Jun 2011 17:55:22 +0100 | Christian Urban | another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy | file | diff | annotate |
| Thu, 23 Jun 2011 22:21:43 +0100 | Christian Urban | the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl | file | diff | annotate |
| Wed, 22 Jun 2011 12:18:22 +0100 | Christian Urban | some rudimentary infrastructure for storing data about nominal datatypes | file | diff | annotate |