Mon, 06 Jun 2011 16:29:13 +0200 kleing atLeastAtMostSuc_conv on int
Mon, 06 Jun 2011 14:11:54 +0200 kleing fixed typo
Sun, 05 Jun 2011 15:00:52 +0200 boehmes updated SMT certificates
Sun, 05 Jun 2011 15:00:17 +0200 boehmes made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)
Fri, 03 Jun 2011 19:37:26 +0200 bulwahn changing the mira setting again for the mutabelle configuration
Fri, 03 Jun 2011 07:25:44 +0200 bulwahn adding more settings to mira's mutabelle configuration
Thu, 02 Jun 2011 15:17:23 +0200 nipkow merged
Thu, 02 Jun 2011 10:10:23 +0200 nipkow Added typed IMP
Thu, 02 Jun 2011 10:13:46 +0200 bulwahn adding quickcheck narrowing to mutabelle script; deactivating nitpick in mutabelle script momentarily because we are not monitoring the results effectively
Thu, 02 Jun 2011 09:51:40 +0200 bulwahn adding invocation of exhaustive testing without using finite types to mutabelle
Thu, 02 Jun 2011 09:51:40 +0200 bulwahn moving the distinction between invocation of testers and generators into test_goal_terms function in quickcheck for its usage with mutabelle
Thu, 02 Jun 2011 08:55:08 +0200 bulwahn splitting Dlist theory in Dlist and Dlist_Cset
Wed, 01 Jun 2011 23:08:04 +0200 nipkow merged
Wed, 01 Jun 2011 22:47:26 +0200 nipkow Made comments text
Wed, 01 Jun 2011 22:42:37 +0200 nipkow Fixed denotational semantics
Wed, 01 Jun 2011 21:50:49 +0200 nipkow Removed old IMP files
Wed, 01 Jun 2011 21:35:34 +0200 nipkow Replacing old IMP with new Semantics material
Wed, 01 Jun 2011 15:53:47 +0200 nipkow tuned lemmas
Wed, 01 Jun 2011 19:50:59 +0200 blanchet fixed debilitating translation bug introduced in b6e61d22fa61 -- "equal" and "=" should always have arity 2
Wed, 01 Jun 2011 13:50:37 +0200 bulwahn setting up code generation for extended reals
Wed, 01 Jun 2011 11:51:25 +0200 nipkow new lemmas
Wed, 01 Jun 2011 10:29:43 +0200 blanchet handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
Wed, 01 Jun 2011 10:29:43 +0200 blanchet more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done
Wed, 01 Jun 2011 10:29:43 +0200 blanchet make sure no warnings are given for polymorphic facts where we use a monomorphic instance
Wed, 01 Jun 2011 10:29:43 +0200 blanchet fixed Isabelle version of lightweight tag theorem, using "Thm.trivial" not "Thm.assume"
Wed, 01 Jun 2011 10:29:43 +0200 blanchet ensured monomorphized facts have normalized zero var indexes, so that "find_var" doesn't fail later on
Wed, 01 Jun 2011 10:29:43 +0200 blanchet fixed interaction between type tags and hAPP in reconstruction code
Wed, 01 Jun 2011 10:29:43 +0200 blanchet implemented missing hAPP and ti cases of new path finder
Wed, 01 Jun 2011 10:29:43 +0200 blanchet support lightweight tags in new Metis
Wed, 01 Jun 2011 10:29:43 +0200 blanchet tuned names
Wed, 01 Jun 2011 10:29:43 +0200 blanchet export one more function
Wed, 01 Jun 2011 10:29:43 +0200 blanchet clausify "<=>" (needed for some type information)
Wed, 01 Jun 2011 10:29:43 +0200 blanchet distinguish different kinds of typing informations in the fact name
Wed, 01 Jun 2011 09:10:13 +0200 bulwahn splitting RBT theory into RBT and RBT_Mapping
Wed, 01 Jun 2011 08:07:28 +0200 bulwahn creating a free variable with proper name and local mixfix syntax (cf. db9b9e46131c)
Wed, 01 Jun 2011 08:07:27 +0200 bulwahn code preprocessor applies simplifier when schematic variables are fixed to free variables to allow rewriting with congruence rules in the preprocessing steps
Wed, 01 Jun 2011 00:23:16 +0200 blanchet make SML/NJ happier
Wed, 01 Jun 2011 00:12:38 +0200 blanchet make sure "Trueprop" is removed before combinators are added -- the code is fragile in that respect
Tue, 31 May 2011 23:39:27 +0200 blanchet speed up example by disabling preplay, and temporarily comment out a broken Sledgehammer call
Tue, 31 May 2011 19:28:03 +0200 boehmes updated SMT certificates
Tue, 31 May 2011 19:27:19 +0200 boehmes proper nesting of loops in new monomorphizer;
Tue, 31 May 2011 19:21:20 +0200 boehmes use new monomorphizer for SMT;
Tue, 31 May 2011 18:13:00 +0200 bulwahn merged
Tue, 31 May 2011 15:45:27 +0200 bulwahn Quickcheck Narrowing only requires one compilation with GHC now
Tue, 31 May 2011 15:45:26 +0200 bulwahn splitting test_goal_terms in Quickcheck into smaller basic functions
Tue, 31 May 2011 15:45:24 +0200 bulwahn adding registration of testers in Quickcheck for its use in Quickcheck_Narrowing
Tue, 31 May 2011 17:15:14 +0200 blanchet compile
Tue, 31 May 2011 17:05:44 +0200 blanchet compile
Tue, 31 May 2011 16:38:36 +0200 blanchet monomorphize in the new Metis if the type system calls for it
Tue, 31 May 2011 16:38:36 +0200 blanchet use "monomorph.ML" in "ATP" theory (so the new Metis can use it)
Tue, 31 May 2011 16:38:36 +0200 blanchet fixed comment
Tue, 31 May 2011 16:38:36 +0200 blanchet fixed new path finder for type information tag
Tue, 31 May 2011 16:38:36 +0200 blanchet no need for type arguments with "xxx_tags_heavy" type system
Tue, 31 May 2011 16:38:36 +0200 blanchet use ":" for type information (looks good in Metis's output) and handle it in new path finder
Tue, 31 May 2011 16:38:36 +0200 blanchet tuned name
Tue, 31 May 2011 16:38:36 +0200 blanchet tuned name
Tue, 31 May 2011 16:38:36 +0200 blanchet make "prepare_atp_problem" more robust w.r.t. choice of type system
Tue, 31 May 2011 16:38:36 +0200 blanchet parse optional type system specification
Tue, 31 May 2011 16:38:36 +0200 blanchet tuning
Tue, 31 May 2011 16:38:36 +0200 blanchet proper handling of type variable classes in new Metis
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip