2009-03-03 nipkow 2009-03-03 removed and renamed redundant lemmas
2009-03-03 wenzelm 2009-03-03 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;
2009-03-03 wenzelm 2009-03-03 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;
2009-03-03 wenzelm 2009-03-03 added markup for binding; tuned;
2009-03-03 wenzelm 2009-03-03 Binding.str_of; removed dead code; tuned;
2009-03-03 wenzelm 2009-03-03 Binding.str_of; pretty_name_atts: check Binding.is_empty, not result of Binding.str_of;
2009-03-03 wenzelm 2009-03-03 Binding.str_of;
2009-03-03 wenzelm 2009-03-03 renamed Binding.display to Binding.str_of, which is slightly more canonical; tuned signature;
2009-03-03 wenzelm 2009-03-03 nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;
2009-03-03 wenzelm 2009-03-03 moved name space externalization flags back to name_space.ML; added pure version extern_flags; do not export internal get_accesses;
2009-03-03 wenzelm 2009-03-03 moved name space externalization flags back to name_space.ML; display: always show prefix for now; tuned signature;
2009-03-03 wenzelm 2009-03-03 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);
2009-03-03 wenzelm 2009-03-03 merged
2009-03-03 wenzelm 2009-03-03 Thm.binding;
2009-03-03 wenzelm 2009-03-03 added type binding and val empty_binding;
2009-03-03 wenzelm 2009-03-03 updated generated files;
2009-03-03 wenzelm 2009-03-03 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;
2009-03-03 Timothy Bourke 2009-03-03 Implement Makarius's suggestion for improved type pattern parsing.
2009-03-02 Timothy Bourke 2009-03-02 find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
2009-03-02 wenzelm 2009-03-02 adapted to lates experimental version; PolyML.Compiler.CPPrintInAlphabeticalOrder false (redundant?);
2009-03-02 wenzelm 2009-03-02 removed Ids;
2009-03-02 haftmann 2009-03-02 merged
2009-03-02 haftmann 2009-03-02 reduced confusion code_funcgr vs. code_wellsorted
2009-03-02 haftmann 2009-03-02 better markup
2009-03-02 nipkow 2009-03-02 name fix
2009-03-02 nipkow 2009-03-02 merged
2009-03-02 nipkow 2009-03-02 name changes
2009-03-02 chaieb 2009-03-02 Automated merge with ssh://chaieb@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
2009-03-02 chaieb 2009-03-02 Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
2009-03-02 wenzelm 2009-03-02 fixed broken @{file} refs;
2009-03-02 wenzelm 2009-03-02 merged
2009-03-02 haftmann 2009-03-02 using plain ISABELLE_PROCESS
2009-03-02 haftmann 2009-03-02 merged
2009-03-02 haftmann 2009-03-02 ignore ISABELLE_LINE_EDITOR for code generation
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2009-03-01 wenzelm 2009-03-01 discontinued experimental support for Alice -- too hard to maintain its many language incompatibilities, never really worked anyway;
2009-03-01 wenzelm 2009-03-01 avoid fragile parsing of end_timing result -- would have produced GC time on MosML, for example;
2009-03-01 wenzelm 2009-03-01 end_timing: generalized result -- message plus with explicit time values;
2009-03-01 wenzelm 2009-03-01 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;
2009-03-01 wenzelm 2009-03-01 updated contributors;
2009-03-01 wenzelm 2009-03-01 removed parts of the manual that are clearly obsolete, or covered by newer manuals already (notably "isar-ref" or "implementation");
2009-03-01 wenzelm 2009-03-01 merged
2009-03-01 wenzelm 2009-03-01 minor update of Mercurial HOWTO;
2009-03-01 nipkow 2009-03-01 removed redundant lemmas
2009-03-01 nipkow 2009-03-01 added lemmas by Jeremy Avigad
2009-02-28 wenzelm 2009-02-28 A Serbian theory, by Filip Maric.
2009-02-28 wenzelm 2009-02-28 more accurate deps;
2009-02-28 wenzelm 2009-02-28 merged
2009-02-28 huffman 2009-02-28 add news for HOLCF; fixed some typos and inaccuracies
2009-02-28 wenzelm 2009-02-28 fixed headers;
2009-02-28 wenzelm 2009-02-28 moved isabelle_system.scala to src/Pure/System/;
2009-02-28 wenzelm 2009-02-28 moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
2009-02-28 wenzelm 2009-02-28 updated generated files;
2009-02-28 wenzelm 2009-02-28 added method "coherent"; tuned formal markup;
2009-02-28 wenzelm 2009-02-28 more refs;
2009-02-28 wenzelm 2009-02-28 moved method "iprover" to HOL specific part;
2009-02-28 wenzelm 2009-02-28 removed Ids;
2009-02-28 wenzelm 2009-02-28 simultaneous use_thys;
2009-02-28 wenzelm 2009-02-28 replaced low-level 'no_syntax' by 'no_notation'; tuned header; tuned proofs;
2009-02-28 wenzelm 2009-02-28 moved generic intuitionistic prover to src/Tools/intuitionistic.ML;