Fri, 18 Jun 2010 14:14:29 +0200 nipkow added lemmas
Fri, 18 Jun 2010 09:04:00 +0200 haftmann dropped dead code
Thu, 17 Jun 2010 19:32:05 +0200 haftmann replaced unreliable metis proof
Thu, 17 Jun 2010 16:15:15 +0200 haftmann rev is reverse in Haskell
Thu, 17 Jun 2010 15:59:48 +0200 haftmann first serious draft of a scala code generator
Thu, 17 Jun 2010 15:59:47 +0200 haftmann more precise code
Thu, 17 Jun 2010 15:59:46 +0200 haftmann explicit type variable arguments for constructors
Thu, 17 Jun 2010 11:33:04 +0200 haftmann transitive superclasses were also only a misunderstanding
Thu, 17 Jun 2010 10:57:00 +0200 haftmann formal introduction of transitive superclasses
Thu, 17 Jun 2010 10:51:38 +0200 haftmann dropped obscure type argument weakening mapping -- was only a misunderstanding
Thu, 17 Jun 2010 10:45:10 +0200 haftmann added simp evaluator
Thu, 17 Jun 2010 10:02:29 +0200 haftmann merged
Tue, 15 Jun 2010 14:28:22 +0200 haftmann added code_simp infrastructure
Tue, 15 Jun 2010 14:28:08 +0200 haftmann tuned whitespace
Tue, 15 Jun 2010 11:38:40 +0200 haftmann maintain cong rules for case combinators; more precise permissiveness
Tue, 15 Jun 2010 11:38:40 +0200 haftmann drop function definitions of combinators
Tue, 15 Jun 2010 11:38:39 +0200 haftmann maintain cong rules for case combinators
Tue, 15 Jun 2010 08:32:32 +0200 haftmann formal introduction of case cong
Tue, 15 Jun 2010 16:42:09 +0200 blanchet found missing beta-eta-contraction
Tue, 15 Jun 2010 16:20:23 +0200 blanchet added missing Umlaut
Tue, 15 Jun 2010 10:47:06 +0200 blanchet make example run a bit faster (might help atbroy102)
Tue, 15 Jun 2010 07:42:48 +0200 haftmann merged
Tue, 15 Jun 2010 07:41:37 +0200 haftmann tuned documents
Mon, 14 Jun 2010 16:00:47 +0200 haftmann teaked naming of superclass projections
Mon, 14 Jun 2010 16:00:46 +0200 haftmann added lemma funpow_mult
Mon, 14 Jun 2010 15:27:11 +0200 haftmann extended bib
Mon, 14 Jun 2010 15:27:09 +0200 haftmann updated generated code
Mon, 14 Jun 2010 15:27:09 +0200 haftmann added reference
Mon, 14 Jun 2010 15:27:08 +0200 haftmann subsection on locale interpretation
Mon, 14 Jun 2010 12:01:30 +0200 haftmann explicitly name and note equations for class eq
Mon, 14 Jun 2010 12:01:30 +0200 haftmann use various predefined Haskell operations when generating code
Mon, 14 Jun 2010 12:01:30 +0200 haftmann NEWS
Mon, 14 Jun 2010 10:50:49 +0200 haftmann tuned internal order
Mon, 14 Jun 2010 10:38:29 +0200 haftmann dropped unused bindings
Mon, 14 Jun 2010 10:38:28 +0200 haftmann corrected syntax diagram
Mon, 14 Jun 2010 21:49:25 +0200 blanchet turn off new polymorphism code again -- a new issue popped up
Mon, 14 Jun 2010 20:48:36 +0200 blanchet missing case
Mon, 14 Jun 2010 20:16:36 +0200 blanchet A function called "untyped_aconv" shouldn't look at the bound names!
Mon, 14 Jun 2010 19:20:32 +0200 blanchet no point in introducing combinators for inlined Skolem functions
Mon, 14 Jun 2010 17:12:41 +0200 blanchet better error reporting for Vampire
Mon, 14 Jun 2010 16:43:44 +0200 blanchet expect SPASS 3.7, and give a friendly warning if an older version is used
Mon, 14 Jun 2010 16:17:20 +0200 blanchet improve ATP-specific error messages
Mon, 14 Jun 2010 15:10:50 +0200 haftmann merged
Mon, 14 Jun 2010 15:10:36 +0200 haftmann removed simplifier congruence rule of "prod_case"
Mon, 14 Jun 2010 10:36:01 +0200 blanchet adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
Sat, 12 Jun 2010 15:48:17 +0200 haftmann merged
Sat, 12 Jun 2010 15:47:50 +0200 haftmann declare lexn.simps [code del]
Fri, 11 Jun 2010 17:14:02 +0200 haftmann declare lex_prod_def [code del]
Fri, 11 Jun 2010 17:14:01 +0200 haftmann modernized specifications
Fri, 11 Jun 2010 17:14:01 +0200 haftmann avoid references to old constdefs
Sat, 12 Jun 2010 11:12:54 +0200 blanchet merged
Sat, 12 Jun 2010 11:12:31 +0200 blanchet disable new polymorphic code for now, until remaining issues in "equality_inf" are resolved
Sat, 12 Jun 2010 11:11:07 +0200 blanchet "raise Fail" for internal errors + one new internal error (instead of "Match")
Fri, 11 Jun 2010 18:05:05 +0200 blanchet make test work again (broken since 09467cdfa198?)
Fri, 11 Jun 2010 17:57:16 +0200 blanchet adjust Nitpick example to follow latest wave of renamings
Fri, 11 Jun 2010 17:10:23 +0200 blanchet proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
Fri, 11 Jun 2010 17:07:27 +0200 blanchet beta-eta-contract, to respect "first_order_match"'s specification;
Fri, 11 Jun 2010 17:05:11 +0200 blanchet adjust Nitpick's handling of "<" on "rat"s and "reals"
Fri, 11 Jun 2010 16:34:56 +0200 blanchet remove needless variables
Fri, 11 Jun 2010 16:52:17 +0200 haftmann hide sum explicitly
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip