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;