Thu, 19 Apr 2007 16:38:59 +0200 | berghofe | nominal_inductive no longer proves equivariance. | changeset | files |
Thu, 19 Apr 2007 16:27:53 +0200 | narboux | add a tactic to generate fresh names | changeset | files |
Wed, 18 Apr 2007 21:30:14 +0200 | wenzelm | simplified ProofContext.infer_types(_pats); | changeset | files |
Wed, 18 Apr 2007 16:23:31 +0200 | dixon | Improved comments. | changeset | files |
Wed, 18 Apr 2007 11:47:08 +0200 | krauss | proper header, added regression tests | changeset | files |
Wed, 18 Apr 2007 11:37:43 +0200 | krauss | added temporary hack to avoid schematic goals in "termination". | changeset | files |