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

Added real related theorems from Fact.thy

Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients

moved upwards in thy graph, real related theorems moved to Transcendental.thy

Enclosed name containing _'s in @{text ...} antiquotation to make document preparation work again.

Added strong congruence rule for UN.

Added abs_def attribute.

removed definition of funpow , reusing that of Relation_Power

Added Formal_Power_Series in imports

A formalization of formal power series

Inserted Formal_Power_Series.thy under Library

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

Minor reorganisation of the Skolemization code

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

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

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

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

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

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

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

Updated comments.

dded theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta

Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta

merged

commented out unused lemmas. May need to be put back by Brian.

-

removed spurious conflic msg

merged

merged - resolving conflics

Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now