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

Repaired a proof that did, after all, refer to the theorem nat_induct2.

merged

Strengthened the induction rule nat_induct2.

Deleted the induction rule nat_induct2, which was too weak and not used even once.

merged

fix to [arith]

new attribute "arith" for facts supplied to arith.

Nicer names in FindTheorems. * Patch NameSpace.get_accesses, contributed by Timothy Bourke: NameSpace.get_accesses has been patched to fix the following bug: theory OverHOL imports Main begin lemma conjI: "a & b --> b" by blast ML {* val ns = PureThy.facts_of @{theory} |> Facts.space_of; val x1 = NameSpace.get_accesses ns "HOL.conjI"; val x2 = NameSpace.get_accesses ns "OverHOL.conjI"; *} end where x1 = ["conjI", "HOL.conjI"] and x2 = ["conjI", "OverHOL.conjI"], but x1 should be just ["HOL.conjI"]. NameSpace.get_accesses is only used within the NameSpace structure itself. The two uses have been modified to retain their original behaviour. Note that NameSpace.valid_accesses gives different results: get_accesses ns "HOL.eq_class.eq" gives ["eq", "eq_class.eq", "HOL.eq_class.eq"] but, valid_accesses ns "HOL.eq_class.eq" gives ["HOL.eq_class.eq", "eq_class.eq", "HOL.eq", "eq"] * Patch FindTheorems: Prefer names that are shorter to type in the current context. * Re-export space_of.

added Determinants to Library

Traces, Determinant of square matrices and some properties

added Euclidean_Space and Glbs to Library

fixed proof -- removed unnecessary sorry

Fixed theorem reference

(Real) Vectors in Euclidean space, and elementary linear algebra.

A generic decision procedure for linear rea arithmetic and normed vector spaces

Permutations, both general and specifically on finite sets.

Imports Main in order to avoid the typerep problem

A theory of greatest lower bounds

Now imports Fact as suggested by Florian in order to avoid the typerep problem

Added HOL/Library/Finite_Cartesian_Product.thy to Library

A formalization of finite cartesian product types

Proof method 'reify' is now reentrant.

added noatps

check for destination directory, do not allocate it gratuitously

Isar proof

merged

code theorems for nth, list_update

added bulkload

code theorems for nth, list_update

added bulkload

added Decision_Procs.thy

merged

session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there

authentic syntax for List.nth

Merged.

Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML + find/fix Product_Type.{fst,snd}, which are now called simply fst and snd.

Automated merge with ssh://chaieb@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle

fixed import

merged

more robust failure in error situations

mandatory prefix for index conversion operations

added replace operation

fixed dependencies : Theory Dense_Linear_Order moved to Library

Theory Dense_Linear_Order moved to Library

fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library

Updated NEWS about approximation

merged

split of already properly working part of Quickcheck infrastructure

code attribute applied before user attributes

moved Random.thy to Library

Add approximation method

Added new Float theory and moved old Library/Float.thy to ComputeFloat

Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series

Make some Refute functions public so I can use them in Nitpick, use @{const_name} antiquotation whenever possible (some, like Lfp.lfp had been renamed since Tjark wrote Refute), and removed some "set"-related code that is no longer relevant in Isabelle2008. There's still some "set" code that needs to be ported; see TODO in the file.

merged

Now catch ERROR exception thrown by find and friends

dropped Id

proper datatype abstraction example

handling type classes without parameters

adjusted theory name

merged

added stub about datatype abstraction

changed name space policy for Haskell includes

merged Big0

added ROOT.ML for Reflection session

merged

established session HOL-Reflection

established session HOL-Reflection

regenerated presburger code

merged Big0

merge

changed default timeout

merged

dropped global Nil/Append interpretation

small fixes; removed Id

mergesort example: recdef->fun, localized

declare "nat o abs" as default measure for int

repaired accidental commit

result for Swing.now;

replaced \overline by \vec;

updated generated files;

tuned;

updated generated files;

removed junk;

improved section "Rule composition"; tuned;

tuned;

improved section on "Hereditary Harrop Formulae";

more on object-level rules; tuned;

updated generated files;

tuned;

more on local theories; tuned;

some text on local theory specifications;

some more Isar macros;

updated genereted files;

minor tuning and typographic fixes;

tuned refs;

removed rudiments of glossary; tuned outline;

removed rudiments of glossary;

removed unused glossary macros;

updated generated files;

observe usual theory naming conventions;

updated generated files;

tuned;

modernized some theory names;

eliminated old 'axclass'; misc tuning and modernization;

avoid redefinition of FIXES/ASSUMES/SHOWS macros;

removed obsolete .cvsignore files;

removed obsolete axclass manual and examples;

explicit section for old/outdated manuals, which are still informative to some extent;

updated generated files;

added introduction; formal markup for "in";

added label;

removed obsolete section "User interfaces"; removed obsolete section "Isabelle/Isar theories", moved parts to beginning of Spec.thy; removed obsolete section "How to write Isar proofs anyway?"; tuned;

tuned spacing;

tuned;

updated generated files;

tuned;

added Isar/VM mode transition diagram;

replaced 'assm' by 'assume' -- regular 'assume' is default, if inference is omitted; tuned;

clean_string/clean_name: proper treatment of \<dash>;

misc tuning;

added section "Canonical reasoning patterns"; tuned;

improved sorry/noproof markup;

tuned;

updated generated files;

added example "First-Order Logic" -- mostly from Trybulec Festschrift;

more on Isar framework -- mostly from Trybulec Festschrift;

more refs;

some more Isar elements;

added "inference" entity;

some more macros;

proof/qed: optional methods;

tuned formal markup;

updated generated files;

added introductory examples;

set quick_and_dirty;

tuned chapter heading;

added parts;

updated generated files;

basic setup for chapter "The Isabelle/Isar Framework";

more refs;

Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.

export lexicographic_order_tac

fix potential incompleteness in SAT encoding

avoid name clash of generated modules and includes

strict check for locale target

fixed proposition slip

added Mapping.thy to Library

dropped Id

updated type class section

updated class documentation

merged

added State_Monad theory in session

proper declared constants in class expressions

merged

added some simp rules

fixed case

Fixed theory name

Added Formal_Power_Series_Examples to HOL-ex image

Some applications of formal power Series