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;

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/;

moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);

updated generated files;

added method "coherent"; tuned formal markup;

more refs;

moved method "iprover" to HOL specific part;

removed Ids;

simultaneous use_thys;

replaced low-level 'no_syntax' by 'no_notation'; tuned header; tuned proofs;

moved generic intuitionistic prover to src/Tools/intuitionistic.ML;

tuned message;

* New prover for coherent logic (see src/Tools/coherent.ML).

more CONTRIBUTORS; fixed some dates;

removed Ids;

moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;

some updates on ancient README;

fixrec package uses new-style syntax and local-theory interface

add function taken_names

merged

make list-style polynomial syntax work when show_sorts is on

more CONTRIBUTORS;

turned "read-only refs" typ_level and minimize_applies into constant values;

merged

removed global ref dfg_format

removed local ref const_needs_hBOOL; renamed some const_min_arity parameters to cma

removed local ref const_min_arity

eliminated private clones of List.partition;

observe some Isabelle/ML coding conventions; avoid structure alias FT, which would complicate systematic searches unnecessarily;