haftmann [Wed, 30 Aug 2006 08:34:45 +0200] rev 20436
added yet another code generator example
haftmann [Wed, 30 Aug 2006 08:30:09 +0200] rev 20435
fixes
haftmann [Wed, 30 Aug 2006 08:29:30 +0200] rev 20434
fixed bug in wfrec appgen
webertj [Wed, 30 Aug 2006 03:30:09 +0200] rev 20433
lin_arith_prover: splitting reverted because of performance loss
webertj [Wed, 30 Aug 2006 03:19:08 +0200] rev 20432
lin_arith_prover: splitting reverted because of performance loss
urbanc [Tue, 29 Aug 2006 21:43:34 +0200] rev 20431
added a FIXME-comment
wenzelm [Tue, 29 Aug 2006 18:56:11 +0200] rev 20430
tuned;
wenzelm [Tue, 29 Aug 2006 18:49:33 +0200] rev 20429
more on contexts;
haftmann [Tue, 29 Aug 2006 14:31:15 +0200] rev 20428
refinements
haftmann [Tue, 29 Aug 2006 14:31:14 +0200] rev 20427
added and refined some exmples
haftmann [Tue, 29 Aug 2006 14:31:13 +0200] rev 20426
added typecopy_package
haftmann [Tue, 29 Aug 2006 14:31:12 +0200] rev 20425
added typecopy_package and some examples
haftmann [Tue, 29 Aug 2006 14:31:11 +0200] rev 20424
updated keywords
paulson [Mon, 28 Aug 2006 18:18:31 +0200] rev 20423
minor bug fixes
paulson [Mon, 28 Aug 2006 18:16:08 +0200] rev 20422
removed the (apparently pointless) signature constraint
paulson [Mon, 28 Aug 2006 18:15:32 +0200] rev 20421
tidied
webertj [Mon, 28 Aug 2006 16:10:44 +0200] rev 20420
encode clauses as Isar premises, rather than as object-logic &, for faster parsing
paulson [Fri, 25 Aug 2006 18:48:58 +0200] rev 20419
abstraction of lambda-expressions
paulson [Fri, 25 Aug 2006 18:48:09 +0200] rev 20418
tidied
paulson [Fri, 25 Aug 2006 18:47:36 +0200] rev 20417
better skolemization, using first-order resolution rather than hoping for the right result
paulson [Fri, 25 Aug 2006 18:46:24 +0200] rev 20416
using inc
paulson [Fri, 25 Aug 2006 18:45:57 +0200] rev 20415
explicit type variables prevent empty sorts
paulson [Fri, 25 Aug 2006 18:44:59 +0200] rev 20414
replaced skolem declarations by automatic skolemization of everything
webertj [Fri, 25 Aug 2006 00:10:10 +0200] rev 20413
avoid duplicate tactics
webertj [Thu, 24 Aug 2006 23:51:46 +0200] rev 20412
additional list of tactics that can be added to arith
berghofe [Thu, 24 Aug 2006 15:20:43 +0200] rev 20411
Added premises concerning finite support of recursion results to FCBs.
huffman [Wed, 23 Aug 2006 23:40:47 +0200] rev 20410
speed up proof of summable_Cauchy
huffman [Wed, 23 Aug 2006 22:44:32 +0200] rev 20409
speed up some proofs
huffman [Wed, 23 Aug 2006 22:12:54 +0200] rev 20408
generalize proof of SUP_rabs_subseq
huffman [Wed, 23 Aug 2006 21:57:43 +0200] rev 20407
speed up some proofs