replaced unreliable metis proof

rev is reverse in Haskell

first serious draft of a scala code generator

more precise code

explicit type variable arguments for constructors

transitive superclasses were also only a misunderstanding

formal introduction of transitive superclasses

dropped obscure type argument weakening mapping -- was only a misunderstanding

added simp evaluator

merged

added code_simp infrastructure

tuned whitespace

maintain cong rules for case combinators; more precise permissiveness

drop function definitions of combinators

maintain cong rules for case combinators

formal introduction of case cong

found missing beta-eta-contraction

added missing Umlaut

make example run a bit faster (might help atbroy102)

merged

tuned documents

teaked naming of superclass projections

added lemma funpow_mult

extended bib

updated generated code

added reference

subsection on locale interpretation

explicitly name and note equations for class eq

use various predefined Haskell operations when generating code

NEWS

tuned internal order

dropped unused bindings

corrected syntax diagram

turn off new polymorphism code again -- a new issue popped up

missing case

A function called "untyped_aconv" shouldn't look at the bound names!

no point in introducing combinators for inlined Skolem functions

better error reporting for Vampire

expect SPASS 3.7, and give a friendly warning if an older version is used

improve ATP-specific error messages

merged

removed simplifier congruence rule of "prod_case"

adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"

merged

declare lexn.simps [code del]

declare lex_prod_def [code del]

modernized specifications

avoid references to old constdefs