| Sat, 26 Mar 2011 12:01:40 +0100 | wenzelm | added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent; | changeset | files |
| Sat, 26 Mar 2011 10:52:29 +0100 | wenzelm | tuned; | changeset | files |
| Sat, 26 Mar 2011 10:25:17 +0100 | wenzelm | dependent_tr': formal treatment of bounds after stripping Abs, although it should only happen for malformed terms, since print_translations work top-down; | changeset | files |
| Thu, 24 Mar 2011 16:56:19 +0100 | wenzelm | added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds; | changeset | files |
| Thu, 24 Mar 2011 16:47:24 +0100 | wenzelm | more direct loose_bvar1; | changeset | files |
| Thu, 24 Mar 2011 13:54:39 +0100 | wenzelm | indentation; | changeset | files |
| Thu, 24 Mar 2011 11:45:39 +0100 | wenzelm | update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees); | changeset | files |