| Wed, 01 Jun 2011 13:50:37 +0200 | bulwahn | setting up code generation for extended reals | changeset | files |
| Wed, 01 Jun 2011 11:51:25 +0200 | nipkow | new lemmas | changeset | files |
| Wed, 01 Jun 2011 10:29:43 +0200 | blanchet | handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes | changeset | files |
| Wed, 01 Jun 2011 10:29:43 +0200 | blanchet | more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done | changeset | files |
| Wed, 01 Jun 2011 10:29:43 +0200 | blanchet | make sure no warnings are given for polymorphic facts where we use a monomorphic instance | changeset | files |
| Wed, 01 Jun 2011 10:29:43 +0200 | blanchet | fixed Isabelle version of lightweight tag theorem, using "Thm.trivial" not "Thm.assume" | changeset | files |