name fix

fix spelling

real_inner class instance for vectors

NEWS

merged

Removed subsumed lemmas

remove duplicated lemmas about norm

real_normed_vector instance

fix real_vector, real_algebra instances

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

add lemma surj_from_nat

fix document generation

merged

fix document generation

section -> subsection

add instance for cancel_comm_monoid_add

add class cancel_comm_monoid_add

more finiteness changes

merged

finiteness lemmas

merged

unset execute bit

Tuned datatype antiquotation.

made SMLNJ happy

typo

find_consts: display the search criteria. (by Timothy Bourke)

find_consts: documentation. (by Timothy Bourke)

FindTheorems solves: update documentation (by Timothy Bourke)

fixed codegen tool

merged

fixed codegen tool

merged

Moved Nat_Int_Bij into Library

removed Reflection session

add lemma add_nonneg_eq_0_iff

add lemmas about sgn

added ML file for the find_consts command

added find_consts to NEWS and CONTRIBUTORS

New command find_consts searching for constants by type (by Timothy Bourke).

fix document generation

move countability proof from Rational to Countable; add instance rat :: countable

Moved FTA into Lib and cleaned it up a little.

ordered_idom instance for polynomials

Export tactic interface for sizechange method

merged

liberal inst_meet

display code theorems with HOL equality

merged

Added serial_string to SAT solver input and output files, to prevent multithreading chaos. Bug reported by Tobias.

Added nitpick_const_simp attribute to recdef and record packages.

Added nitpick_const_simp attribute to 'simps' produced by the old primrec package.

Renamed descriptions of Nitpick (and ATP) attributes, so that they fit well with the rest of the sentence in ProofGeneral.

Reintroduced nitpick_ind_intro attribute. It looks like I need it nonetheless.

merged

Added Nitpick_Const_Psimp attribute, dropped the 's' in Nitpick_Const_Simps, and killed the Nitpick_Ind_Intros attribute. This should now be all.

merged

Merged.

Added "nitpick_const_simps" and "nitpick_ind_intros" attributes for theorems; these will be used by Nitpick, which will be released independently of Isabelle 2009, but they need to be in.

fixed typo

updated NEWS etc with "solves" criterion and auto_solves

merged

Moved Order_Relation into Library and moved some of it into Relation.

Autosolve feature for detecting duplicate theorems; patch by Timothy Bourke

FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke

const_name antiquotations