Fri, 19 Jan 2007 15:13:47 +0100 chaieb Theorem "(x::int) dvd 1 = ( ¦x¦ = 1)" added to default simpset.
Fri, 19 Jan 2007 13:16:37 +0100 wenzelm adapted ML context operations;
Fri, 19 Jan 2007 13:09:37 +0100 wenzelm added generic_theory_of;
Fri, 19 Jan 2007 13:09:36 +0100 wenzelm added 'declaration' command;
Fri, 19 Jan 2007 13:09:35 +0100 wenzelm added 'declaration' command;
Fri, 19 Jan 2007 13:09:33 +0100 wenzelm adapted ML context operations;
Fri, 19 Jan 2007 13:09:32 +0100 wenzelm ML context: full generic context, tuned signature;
Fri, 19 Jan 2007 13:09:31 +0100 wenzelm updated
Thu, 18 Jan 2007 11:16:49 +0100 aspinall Fix pgmlsymbolsoff
Wed, 17 Jan 2007 19:29:55 +0100 urbanc tuned a bit the proofs
Wed, 17 Jan 2007 11:39:32 +0100 dixon correctled left/right following of another context in zipto.
Wed, 17 Jan 2007 09:53:50 +0100 paulson induction rules for trancl/rtrancl expressed using subsets
Wed, 17 Jan 2007 09:52:54 +0100 paulson Deleted mk_fol_type, since the constructors can be used directly
Wed, 17 Jan 2007 09:52:06 +0100 paulson Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
Tue, 16 Jan 2007 14:11:25 +0100 urbanc fixed typo introduced by me
Tue, 16 Jan 2007 14:10:27 +0100 haftmann changed dictionary representation to explicit classrel witnesses
Tue, 16 Jan 2007 14:10:26 +0100 haftmann reverted order of classrels
Tue, 16 Jan 2007 14:10:24 +0100 haftmann cleanup
Tue, 16 Jan 2007 13:59:08 +0100 urbanc formalisation of Crary's chapter on logical relations
Tue, 16 Jan 2007 10:25:38 +0100 urbanc added capabilities to handle mutual inductions
Tue, 16 Jan 2007 08:12:09 +0100 haftmann refined and added example for ExecutableRat
Tue, 16 Jan 2007 08:07:00 +0100 haftmann introduced binding concept
Tue, 16 Jan 2007 08:06:59 +0100 haftmann slight cleanup
Tue, 16 Jan 2007 08:06:57 +0100 haftmann renamed locale partial_order to order
Tue, 16 Jan 2007 08:06:55 +0100 haftmann refined and added example for ExecutableRat
Tue, 16 Jan 2007 08:06:52 +0100 haftmann updated keywords
Mon, 15 Jan 2007 10:15:55 +0100 krauss added sections on mutual induction and patterns
Sun, 14 Jan 2007 09:57:29 +0100 paulson optimized translation of HO problems
Fri, 12 Jan 2007 15:37:21 +0100 ballarin Reverted to structure representation with records.
Fri, 12 Jan 2007 09:58:31 +0100 haftmann more term inspection
Fri, 12 Jan 2007 09:58:30 +0100 haftmann introduced binding concept
Fri, 12 Jan 2007 09:58:29 +0100 haftmann adjusted manual
Thu, 11 Jan 2007 16:53:12 +0100 paulson well-founded relations for the integers
Thu, 11 Jan 2007 01:34:23 +0100 webertj updated to mention the automatic unfolding of constants
Wed, 10 Jan 2007 20:17:26 +0100 wenzelm removed NameSpace.split -- use qualifier/base instead;
Wed, 10 Jan 2007 20:16:52 +0100 wenzelm fixed exit: proper type check of state;
Wed, 10 Jan 2007 19:19:24 +0100 webertj tuned
Wed, 10 Jan 2007 19:18:29 +0100 webertj minor comment change
Wed, 10 Jan 2007 19:17:52 +0100 webertj no unfolding necessary anymore (refute does that automatically now)
Wed, 10 Jan 2007 09:28:24 +0100 haftmann improved case patterns
Wed, 10 Jan 2007 08:58:35 +0100 haftmann added undefined in cases
Tue, 09 Jan 2007 19:09:01 +0100 haftmann named preprocessorts
Tue, 09 Jan 2007 19:09:00 +0100 haftmann cleanup
Tue, 09 Jan 2007 19:08:59 +0100 haftmann activated new class code
Tue, 09 Jan 2007 19:08:58 +0100 haftmann handling for "undefined" in case expressions
Tue, 09 Jan 2007 19:08:56 +0100 haftmann named preprocessors
Tue, 09 Jan 2007 18:13:55 +0100 paulson The "of 1, simplified" stopped working some time ago, leaving these simprules
Tue, 09 Jan 2007 18:12:59 +0100 paulson More compact proof reconstruction: lines having fewer than !min_deps dependences are folded
Tue, 09 Jan 2007 15:49:39 +0100 paulson simplified the resoution proofs
Tue, 09 Jan 2007 12:12:00 +0100 aspinall Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
Tue, 09 Jan 2007 12:09:49 +0100 aspinall Add info fatality for error messages.
Tue, 09 Jan 2007 12:09:21 +0100 aspinall Add informfileoutdated and completed flag. This makes the PGIP messages match the Broker states.
Tue, 09 Jan 2007 08:32:50 +0100 haftmann slight cleanups
Tue, 09 Jan 2007 08:31:54 +0100 haftmann improved names
Tue, 09 Jan 2007 08:31:52 +0100 haftmann proper node names
Tue, 09 Jan 2007 08:31:51 +0100 haftmann slight cleanup
Tue, 09 Jan 2007 08:31:50 +0100 haftmann improved variable name handling
Tue, 09 Jan 2007 08:31:49 +0100 haftmann moved variable environments here
Tue, 09 Jan 2007 08:31:48 +0100 haftmann moved a lot to codegen_func.ML
Tue, 09 Jan 2007 08:31:47 +0100 haftmann typo
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip