| Wed, 01 Jun 2011 10:29:43 +0200 | blanchet | fixed Isabelle version of lightweight tag theorem, using "Thm.trivial" not "Thm.assume" | changeset | files |
| Wed, 01 Jun 2011 10:29:43 +0200 | blanchet | ensured monomorphized facts have normalized zero var indexes, so that "find_var" doesn't fail later on | changeset | files |
| Wed, 01 Jun 2011 10:29:43 +0200 | blanchet | fixed interaction between type tags and hAPP in reconstruction code | changeset | files |
| Wed, 01 Jun 2011 10:29:43 +0200 | blanchet | implemented missing hAPP and ti cases of new path finder | changeset | files |
| Wed, 01 Jun 2011 10:29:43 +0200 | blanchet | support lightweight tags in new Metis | changeset | files |
| Wed, 01 Jun 2011 10:29:43 +0200 | blanchet | tuned names | changeset | files |
| Wed, 01 Jun 2011 10:29:43 +0200 | blanchet | export one more function | changeset | files |