Tue, 31 May 2011 16:38:36 +0200 | blanchet | use "monomorph.ML" in "ATP" theory (so the new Metis can use it) | changeset | files |
Tue, 31 May 2011 16:38:36 +0200 | blanchet | fixed comment | changeset | files |
Tue, 31 May 2011 16:38:36 +0200 | blanchet | fixed new path finder for type information tag | changeset | files |
Tue, 31 May 2011 16:38:36 +0200 | blanchet | no need for type arguments with "xxx_tags_heavy" type system | changeset | files |
Tue, 31 May 2011 16:38:36 +0200 | blanchet | use ":" for type information (looks good in Metis's output) and handle it in new path finder | changeset | files |
Tue, 31 May 2011 16:38:36 +0200 | blanchet | tuned name | changeset | files |