Wed, 19 May 2004 11:30:18 +0200 | paulson | more results about isomorphisms | changeset | files |
Wed, 19 May 2004 11:29:47 +0200 | paulson | conversion of Hilbert_Choice to Isar script | changeset | files |
Wed, 19 May 2004 11:24:54 +0200 | chaieb | the function list1 has been exported. | changeset | files |
Wed, 19 May 2004 11:23:59 +0200 | chaieb | A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller. | changeset | files |
Wed, 19 May 2004 11:21:19 +0200 | chaieb | tactic call changed from TRYALL arith_tac to TRYALL simple_arith_tac preventing a call to presburger. | changeset | files |
Tue, 18 May 2004 11:45:50 +0200 | obua | modified abel_cancel.ML for polymorphic types | changeset | files |
Tue, 18 May 2004 10:02:50 +0200 | obua | simplification for abelian groups | changeset | files |
Tue, 18 May 2004 10:01:44 +0200 | obua | Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy | changeset | files |