Wed, 05 Feb 2014 23:30:02 +0100 | blanchet | adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas | changeset | files |
Wed, 05 Feb 2014 18:19:25 +0100 | blanchet | merge | changeset | files |
Wed, 05 Feb 2014 17:59:12 +0100 | blanchet | properly massage 'if's / 'case's etc. under lambdas | changeset | files |
Wed, 05 Feb 2014 17:07:22 +0000 | paulson | Merge | changeset | files |
Wed, 05 Feb 2014 17:06:11 +0000 | paulson | Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs. | changeset | files |
Wed, 05 Feb 2014 16:33:22 +0100 | blanchet | fixed handling of 'split' | changeset | files |
Wed, 05 Feb 2014 15:44:32 +0100 | Lars Hupel | made SML/NJ happy | changeset | files |