Added a "nitpick_maybe" symbol, which is used by Nitpick. This will go away once Nitpick is part of HOL.

merged

merged

set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax

merged

set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax

tuned

moved complete_lattice to Set.thy

dropped Id

corrected slip in NEWS

merged

added strict_mono predicate

Identifiers of some old CVS file versions;

recovered generated files;

more precise deps;

merged

Added Docs

render_tree: suppress markup only for empty body (of status messages, cf. da275b7809bd) in order to recover hilite;

removed obsolete claset_rules_of, simpset_rules_of -- as proposed in the text;

removed unused TableFun().fold_map and GraphFun().fold_map_nodes;

removed spurious occurrences of old rep_ss;

Thm.add_oracle interface: replaced old bstring by binding;

silent chmod;

Consts.abbreviate: reject schematic term variables, prevent schematic type variables (hidden polymorphism) via Term.close_schematic_term -- see also 8f84a608883d;

close_schematic_term: uniform order of types/terms; tuned;

eliminated Consts.eq_consts tuning -- this is built into tables and name spaces already;

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

renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify; minor tuning;

moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings; moved separator/is_qualified from binding.ML back to name_space.ML -- only name space introduces an explicit notation for qualified names; type binding: maintain explicit qualifier, indepently of base name; tuned signature of Binding: renamed name_pos to make, renamed base_name to name_of, renamed map_base to map_name, added mandatory flag to qualify, simplified map_prefix (formerly unused); Binding.str_of: include markup with position properties; misc tuning;

added markup for binding; tuned;

Binding.str_of; removed dead code; tuned;

Binding.str_of; pretty_name_atts: check Binding.is_empty, not result of Binding.str_of;

Binding.str_of;

renamed Binding.display to Binding.str_of, which is slightly more canonical; tuned signature;

nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;

moved name space externalization flags back to name_space.ML; added pure version extern_flags; do not export internal get_accesses;

moved name space externalization flags back to name_space.ML; display: always show prefix for now; tuned signature;

reverted change introduced in a7c164e228e1 -- there cannot be a "bug" in a perfectly normal operation on the internal data representation that merely escaped into public by accident (cf. 0a981c596372);

merged

Thm.binding;

added type binding and val empty_binding;

updated generated files;

ignore "source" option in antiquotations @{ML}, @{ML_type}, @{ML_struct} -- did not really make sense, without it users can enable source mode globally with less surprises;

Implement Makarius's suggestion for improved type pattern parsing.

find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch

adapted to lates experimental version; PolyML.Compiler.CPPrintInAlphabeticalOrder false (redundant?);

removed Ids;

merged

reduced confusion code_funcgr vs. code_wellsorted

better markup

name fix

merged

name changes

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

Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy

fixed broken @{file} refs;

merged

using plain ISABELLE_PROCESS

merged

ignore ISABELLE_LINE_EDITOR for code generation

use long names for old-style fold combinators;