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;

discontinued experimental support for Alice -- too hard to maintain its many language incompatibilities, never really worked anyway;

avoid fragile parsing of end_timing result -- would have produced GC time on MosML, for example;

end_timing: generalized result -- message plus with explicit time values;

replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already); minor tuning according to Isabelle coding conventions;

updated contributors;

removed parts of the manual that are clearly obsolete, or covered by newer manuals already (notably "isar-ref" or "implementation");

merged

minor update of Mercurial HOWTO;

removed redundant lemmas

added lemmas by Jeremy Avigad

A Serbian theory, by Filip Maric.

more accurate deps;

merged

add news for HOLCF; fixed some typos and inaccuracies

fixed headers;

moved isabelle_system.scala to src/Pure/System/;