wenzelm [Fri, 21 May 2004 21:14:18 +0200] rev 14765
proper use of 'syntax';
paulson [Wed, 19 May 2004 11:41:58 +0200] rev 14764
auto update
paulson [Wed, 19 May 2004 11:31:26 +0200] rev 14763
has_consts now handles the @-operator
paulson [Wed, 19 May 2004 11:30:56 +0200] rev 14762
new bij_betw operator
paulson [Wed, 19 May 2004 11:30:18 +0200] rev 14761
more results about isomorphisms
paulson [Wed, 19 May 2004 11:29:47 +0200] rev 14760
conversion of Hilbert_Choice to Isar script
chaieb [Wed, 19 May 2004 11:24:54 +0200] rev 14759
the function list1 has been exported.
chaieb [Wed, 19 May 2004 11:23:59 +0200] rev 14758
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.
chaieb [Wed, 19 May 2004 11:21:19 +0200] rev 14757
tactic call changed from TRYALL arith_tac to TRYALL simple_arith_tac preventing a call to presburger.
obua [Tue, 18 May 2004 11:45:50 +0200] rev 14756
modified abel_cancel.ML for polymorphic types