| Mon, 09 May 2011 16:11:20 +0200 | noschinl | add a lemma about commutative append to List.thy | changeset | files |
| Mon, 09 May 2011 12:26:25 +0200 | noschinl | removed assumption from lemma List.take_add | changeset | files |
| Fri, 06 May 2011 20:25:41 +0200 | wenzelm | no need for underscore.sty -- latex.ltx provides \textunderscore and \_ already; | changeset | files |
| Fri, 06 May 2011 17:52:08 +0200 | wenzelm | removed \underscoreon which is from Larry's iman.sty, not underscore.sty; | changeset | files |
| Fri, 06 May 2011 13:35:00 +0200 | blanchet | further improved type system setup based on Judgment Days | changeset | files |
| Fri, 06 May 2011 13:34:59 +0200 | blanchet | allow each prover to specify its own formula kind for symbols occurring in the conjecture | changeset | files |
| Fri, 06 May 2011 13:34:59 +0200 | blanchet | better type system setup, based on Judgment Day | changeset | files |