isabelle: Changelog

Mercurial Mercurial > repos > isabelle / changelog

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -10000 -3000 -1000 -300 -100 -50 -32 +32 +50 +100 +300 +1000 +3000 +10000 +30000 tip

Tue, 29 Aug 2006 14:31:11 +0200 updated keywords

haftmann [Tue, 29 Aug 2006 14:31:11 +0200] rev 20424

updated keywords

Mon, 28 Aug 2006 18:18:31 +0200 minor bug fixes

paulson [Mon, 28 Aug 2006 18:18:31 +0200] rev 20423

minor bug fixes

Mon, 28 Aug 2006 18:16:08 +0200 removed the (apparently pointless) signature constraint

paulson [Mon, 28 Aug 2006 18:16:08 +0200] rev 20422

removed the (apparently pointless) signature constraint

Mon, 28 Aug 2006 18:15:32 +0200 tidied

paulson [Mon, 28 Aug 2006 18:15:32 +0200] rev 20421

tidied

Mon, 28 Aug 2006 16:10:44 +0200 encode clauses as Isar premises, rather than as object-logic &, for faster parsing

webertj [Mon, 28 Aug 2006 16:10:44 +0200] rev 20420

encode clauses as Isar premises, rather than as object-logic &, for faster parsing

Fri, 25 Aug 2006 18:48:58 +0200 abstraction of lambda-expressions

paulson [Fri, 25 Aug 2006 18:48:58 +0200] rev 20419

abstraction of lambda-expressions

Fri, 25 Aug 2006 18:48:09 +0200 tidied

paulson [Fri, 25 Aug 2006 18:48:09 +0200] rev 20418

tidied

Fri, 25 Aug 2006 18:47:36 +0200 better skolemization, using first-order resolution rather than hoping for the right result

paulson [Fri, 25 Aug 2006 18:47:36 +0200] rev 20417

better skolemization, using first-order resolution rather than hoping for the right result

Fri, 25 Aug 2006 18:46:24 +0200 using inc

paulson [Fri, 25 Aug 2006 18:46:24 +0200] rev 20416

using inc

Fri, 25 Aug 2006 18:45:57 +0200 explicit type variables prevent empty sorts

paulson [Fri, 25 Aug 2006 18:45:57 +0200] rev 20415

explicit type variables prevent empty sorts

Fri, 25 Aug 2006 18:44:59 +0200 replaced skolem declarations by automatic skolemization of everything

paulson [Fri, 25 Aug 2006 18:44:59 +0200] rev 20414

replaced skolem declarations by automatic skolemization of everything

Fri, 25 Aug 2006 00:10:10 +0200 avoid duplicate tactics

webertj [Fri, 25 Aug 2006 00:10:10 +0200] rev 20413

avoid duplicate tactics

Thu, 24 Aug 2006 23:51:46 +0200 additional list of tactics that can be added to arith

webertj [Thu, 24 Aug 2006 23:51:46 +0200] rev 20412

additional list of tactics that can be added to arith

Thu, 24 Aug 2006 15:20:43 +0200 Added premises concerning finite support of recursion results to FCBs.

berghofe [Thu, 24 Aug 2006 15:20:43 +0200] rev 20411

Added premises concerning finite support of recursion results to FCBs.

Wed, 23 Aug 2006 23:40:47 +0200 speed up proof of summable_Cauchy

huffman [Wed, 23 Aug 2006 23:40:47 +0200] rev 20410

speed up proof of summable_Cauchy

Wed, 23 Aug 2006 22:44:32 +0200 speed up some proofs

huffman [Wed, 23 Aug 2006 22:44:32 +0200] rev 20409

speed up some proofs

Wed, 23 Aug 2006 22:12:54 +0200 generalize proof of SUP_rabs_subseq

huffman [Wed, 23 Aug 2006 22:12:54 +0200] rev 20408

generalize proof of SUP_rabs_subseq

Wed, 23 Aug 2006 21:57:43 +0200 speed up some proofs

huffman [Wed, 23 Aug 2006 21:57:43 +0200] rev 20407

speed up some proofs

Wed, 23 Aug 2006 17:05:08 +0200 SML/NJ int type fix

haftmann [Wed, 23 Aug 2006 17:05:08 +0200] rev 20406

SML/NJ int type fix

Mon, 21 Aug 2006 11:02:44 +0200 tracing

haftmann [Mon, 21 Aug 2006 11:02:44 +0200] rev 20405

tracing

Mon, 21 Aug 2006 11:02:43 +0200 improved preprocessing

haftmann [Mon, 21 Aug 2006 11:02:43 +0200] rev 20404

improved preprocessing

Mon, 21 Aug 2006 11:02:42 +0200 fixed bug in sortlookup

haftmann [Mon, 21 Aug 2006 11:02:42 +0200] rev 20403

fixed bug in sortlookup

Mon, 21 Aug 2006 11:02:41 +0200 more concise preprocessing of numerals for code generation

haftmann [Mon, 21 Aug 2006 11:02:41 +0200] rev 20402

more concise preprocessing of numerals for code generation

Mon, 21 Aug 2006 11:02:40 +0200 more concise string serialization

haftmann [Mon, 21 Aug 2006 11:02:40 +0200] rev 20401

more concise string serialization

Mon, 21 Aug 2006 11:02:39 +0200 added some codegen examples/applications

haftmann [Mon, 21 Aug 2006 11:02:39 +0200] rev 20400

added some codegen examples/applications

Fri, 18 Aug 2006 18:51:44 +0200 adapted using the characteristic equations

urbanc [Fri, 18 Aug 2006 18:51:44 +0200] rev 20399

adapted using the characteristic equations

Fri, 18 Aug 2006 18:46:02 +0200 modified to use the characteristic equations

urbanc [Fri, 18 Aug 2006 18:46:02 +0200] rev 20398

modified to use the characteristic equations

Fri, 18 Aug 2006 17:03:23 +0200 - Fixed bug that caused uniqueness proof for recursion

berghofe [Fri, 18 Aug 2006 17:03:23 +0200] rev 20397

- Fixed bug that caused uniqueness proof for recursion combinator to fail for mutually recursive datatypes - Implemented proofs of characteristic equations for recursion combinator.

Thu, 17 Aug 2006 20:31:36 +0200 used the recursion combinator for the height and substitution function

urbanc [Thu, 17 Aug 2006 20:31:36 +0200] rev 20396

used the recursion combinator for the height and substitution function

Thu, 17 Aug 2006 19:20:43 +0200 added definition for size and substitution using the recursion

urbanc [Thu, 17 Aug 2006 19:20:43 +0200] rev 20395

added definition for size and substitution using the recursion combinator

Thu, 17 Aug 2006 09:24:56 +0200 improved thmtab

haftmann [Thu, 17 Aug 2006 09:24:56 +0200] rev 20394

improved thmtab

Thu, 17 Aug 2006 09:24:51 +0200 fixed bug in sortcontext extraction

haftmann [Thu, 17 Aug 2006 09:24:51 +0200] rev 20393

fixed bug in sortcontext extraction

(0) -10000 -3000 -1000 -300 -100 -50 -32 +32 +50 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle