| Fri, 21 Sep 2012 16:34:40 +0200 | blanchet | renamed top-level theory from "Codatatype" to "BNF" | file | diff | annotate |
| Thu, 20 Sep 2012 02:42:49 +0200 | blanchet | provide predicator, define relator | file | diff | annotate |
| Wed, 12 Sep 2012 06:35:07 +0200 | blanchet | reduced theory dependencies | file | diff | annotate |
| Wed, 12 Sep 2012 06:30:35 +0200 | blanchet | tuning | file | diff | annotate |
| Wed, 12 Sep 2012 06:27:48 +0200 | blanchet | moved theorems closer to where they are used | file | diff | annotate |
| Wed, 12 Sep 2012 05:29:21 +0200 | blanchet | renamed "Ordinals_and_Cardinals" to "Cardinals" | file | diff | annotate |
| Wed, 12 Sep 2012 05:21:47 +0200 | blanchet | split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF | file | diff | annotate |
| Tue, 11 Sep 2012 17:14:49 +0200 | blanchet | move "bnf_util.ML" to "BNF_Util.thy" | file | diff | annotate |
| Tue, 11 Sep 2012 17:09:39 +0200 | blanchet | renamed "BNF_Library" to "BNF_Util" | file | diff | annotate | base |