merged

generalize lemmas from nat to 'a::wellorder

generalize some lemmas

merged

removed redundant thms

merged

class instances for num1

Removed redundant lemmas

merged

also consider superclasses properly

merged

removed subsumed lemmas

merged

datatype antiquotation: always bracket types with spaces in between

consequent use of term `code equation`

permissive check for pattern discipline in case schemes

maintain order of constructors in datatypes; clarified conventions for type schemes

stripped Id

merged

add theory of products as real vector spaces to Library

add new theory Product_plus.thy to Library

merged

changed message

detailed information on atp-failure via Output.debug

merged

reverted to old wellsorting algorithm

fixed spurious proof failure

consider changes variable names in theorem le_imp_power_dvd

tuned and incremental version of wellsorting algorithm

ignore sorts in bare types

defensive implementation of pretty serialisation of lists and characters

dropped Id

experimental inclusion of new wellsorting algorithm for code equations

merged

merged

merged

fixed selection of premises

cleaned up

declare of_int_number_of_eq [simp]

fix case_names

nicer induction/cases rules for numeral types

number_ring instances for numeral types

declare xor_compl_{left,right} [simp]

add rule for minus 1 at type bit

add formalization of a type of integers mod 2 to Library

new theory of real inner product spaces

add Powerdomain_ex.thy

add more ordering lemmas

avoid using ab_semigroup_idem_mult locale for powerdomains

merged

add header

move Polynomial.thy to Library

move FrechetDeriv.thy to Library

split polynomial-related stuff from Deriv.thy into Library/Poly_Deriv.thy

half auto_solve default time out; increase manually in PG for large projects (L4v/Verisoft large).

merged

finish converting Deriv.thy to new polynomial library

generalize int_dvd_cancel_factor simproc to idom class

composition of polynomials

add some lemmas, cleaned up

generalize le_imp_power_dvd and power_le_dvd; move from Divides to Power

move polynomial order stuff from Fundamental_Theorem_Algebra to Polynomial

merged

more subsection headings

speed up proof of exp_exists

tuned

sort instances wrt. to class hierarchy

fixed signature

tuned accessor name

more precise improvement in instantiation user space type system

do not drop arguments to 0, 1

merged

reverted to previous version of Finite_Set.thy

merged

merged

first working version

tuned comments, stripped ID, deleted superfluous code

stripped ID

Syntactic support for products over set intervals

No idea what happened here!

Even and odd powers of -1

merged

Reintroduce set_interpreter for Collect and op :. I removed them by accident when removing old code that dealt with the "set" type. Incidentally, there is still some broken "set" code in Refute that should be fixed (see TODO in refute.ML).

Added Nitpick tag to 'of_int_of_nat'. This theorem leads to a more efficient encoding to Kodkod than the definition of 'of_int'.

add lemmas for exponentiation

merged

unified variable names in case expressions; no exponential fork in translation of case expressions

merged

remove redundant simp attributes for zdvd rules

lemmas abs_dvd_iff, dvd_abs_iff

Cleaned up IntDiv and removed subsumed lemmas.

tune section headings; add square function

merged

rearrange subsections

remove instances num::semiring and num::linorder

datatype num = One | Dig0 num | Dig1 num

replace 1::num with One; remove monoid_mult instance

replace dec with double-and-decrement function

more default simp rules for sgn

re-generated

clarified import

faster preprocessor

added pdivmod on int (for code generation)

merged

tuned texts

dropped Id

dropped clause_suc_preproc for generic code generator

new primrec

Adapted to encoding of sets as predicates.

enable auto-solve by default

merged

Added nitpick attribute, and fixed typo.

Added myself to testing list.

dvd and setprod lemmas

merged

added finite_set_choice

reject defined function in patterns with errmsg, e.g. f (f x) = x

fixed document

more finiteness

merged

more finiteness

merged

more finiteness

generalize lemma fps_square_eq_iff, move to Ring_and_Field

generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup

add mult_delta lemmas; simplify some proofs

fix spelling

declare fps_nth as a typedef morphism; clean up instance proofs