TableFun.join/merge: optimize the important special case where the tables coincide -- NOTE: this changes both the operational behaviour and the result for non-standard join/eq notion;

fixed proofs -- follow-up to ecd6f0ca62ea;

renamed NameSpace.base to NameSpace.base_name (in accordance with "full_name"); tuned;

renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;

eliminated obsolete ProofContext.full_bname;

Binding.prefix_of;

adapted Binding.dest; tuned;

added prefix_of; tuned signature; tuned;

Reintroduced previous changes: Made "Refute.norm_rhs" public and simplified the configuration of the BerkMin and zChaff SAT solvers.

merged

declare power_Suc [simp]; remove redundant type-specific versions of power_Suc

regenerated document;

merge with dummy changeset, to recover files in doc-src/IsarImplementation/ which got lost in aea5d7fa7ef5 (potentially due to insensitive file system on Mac OS);

dummy changes to produce a new changeset of these files;

updated generated file -- changed since @{ML} now ignores source flag;

fixed document;

removed old/broken CVS Ids;

ML antiquotation @{lemma}: allow 'and' list, proper simultaneous type-checking;

merged

Moved general theorems about sums and products to FiniteSet.thy

fixed proofs; added rules as default simp-rules

A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms

Added Libray dependency on Topology_Euclidean_Space

Added general theorems for fold_image, setsum and set_prod

fixed proofs

merged

merged

merged

merged

Second try at adding "nitpick_const_def" attribute. I don't know what happened the first time (change d8944fd4365e). It just vanished somehow.

Fix parentheses.

merged

Added "nitpick_const_simp" attribute to Nominal primrec.

NEWS: renamed o2s to Option.set;

less arbitrary occurrences of undefined

datatype antiquotation does not assume LaTeX as output any longer

merged

Option.thy

consequent rewrite of index_size, size [index] to nat_of; support pseudo-primrec sepcifications with fun

merged

explicit error message for `improper` instances lacking explicit instance parameter constants

Merge.

Merge.

Merge.

Made Refute.norm_rhs public, so I can use it in Nitpick.

Added "nitpick_const_def" attribute, for overriding the definition axiom of a constant.

Eliminated ZCHAFF_VERSION configuration variable, since zChaff's output format is identical in all versions since March 2003 (at least), and also because it forces users who want to use the latest versions to lie about the version number. I also made the BERKMIN_EXE variable optional, defaulting to BerkMin561 (a reasonable name with no platform encoded in it). These changes have no inpacts on already working Isabelle installations.

merged

Made Option a separate theory and renamed option_map to Option.map

renamed Method.assumption_tac back to Method.assm_tac -- as assumption_tac it would have to be exactly the tactic behind the assumption method (with facts);

eliminated internal stamp equality, replaced by bare-metal pointer_eq; misc tuning and polishing;

tuned str_of, now subject to verbose flag;

added @{binding} ML antiquotations;

added print_properties, print_position (again);

merged

merged

tuned manuals

more canonical directory structure of manuals

merged

removed and renamed redundant lemmas