Wed, 29 May 2013 23:11:21 +0200 | wenzelm | obsolete; | changeset | files |
Wed, 29 May 2013 18:55:37 +0200 | wenzelm | resolve_inc_tyvars: back to old behavior before 0fa3b456a267 where types of equal Vars are *not* unified -- recover last example in src/HOL/Metis_Examples/Clausification.thy; | changeset | files |