2010-03-10 haftmann 2010-03-10 split off theory Big_Operators from theory Finite_Set
2010-03-11 blanchet 2010-03-11 moved some Nitpick code around
2010-03-11 wenzelm 2010-03-11 more basic Local_Defs.export_cterm;
2010-03-11 wenzelm 2010-03-11 tuned signature;
2010-03-11 wenzelm 2010-03-11 tuned;
2010-03-11 wenzelm 2010-03-11 actually apply morphism to binding;
2010-03-11 wenzelm 2010-03-11 absolute lib_path relative to ML_HOME -- for improved robustness; explicit warning if shared library failed to load;
2010-03-11 blanchet 2010-03-11 added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
2010-03-11 blanchet 2010-03-11 added term postprocessor to Nitpick, to provide custom syntax for typedefs
2010-03-11 blanchet 2010-03-11 made "Manual_Nits" tests more robust
2010-03-11 haftmann 2010-03-11 merged
2010-03-11 haftmann 2010-03-11 made smlnj happy
2010-03-10 huffman 2010-03-10 replace Nat_Int_Bij with Nat_Bijection in ROOT.ML
2010-03-10 huffman 2010-03-10 remove obsolete theory Nat_Int_Bij
2010-03-10 huffman 2010-03-10 switch from Nat_Int_Bij to Nat_Bijection
2010-03-10 huffman 2010-03-10 convert HOL-Probability to use Nat_Bijection library
2010-03-10 huffman 2010-03-10 convert SET_Protocol to use Nat_Bijection library
2010-03-10 huffman 2010-03-10 convert TLS to use Nat_Bijection library
2010-03-10 huffman 2010-03-10 adapt HOLCF to use Nat_Bijection library
2010-03-10 huffman 2010-03-10 new theory Library/Nat_Bijection.thy
2010-03-10 blanchet 2010-03-10 improve precision of "card" in Nitpick
2010-03-10 blanchet 2010-03-10 merged
2010-03-10 blanchet 2010-03-10 merged
2010-03-10 blanchet 2010-03-10 show nice error message in Nitpick when "java" is not available
2010-03-10 blanchet 2010-03-10 fixed soundness bug in Nitpick
2010-03-10 hoelzl 2010-03-10 merged
2010-03-09 hoelzl 2010-03-09 Use same order of neq-elimination as in proof search.
2010-03-08 hoelzl 2010-03-08 Moved theorems in Lebesgue to the right places
2010-03-10 haftmann 2010-03-10 constdefs is legacy
2010-03-10 haftmann 2010-03-10 recdef is legacy
2010-03-10 haftmann 2010-03-10 fixed typo
2010-03-10 haftmann 2010-03-10 avoid confusion
2010-03-10 haftmann 2010-03-10 tuned whitespace
2010-03-10 haftmann 2010-03-10 merged
2010-03-10 haftmann 2010-03-10 tuned
2010-03-09 haftmann 2010-03-09 clarified transfer code proper; more natural declaration of return rules
2010-03-09 haftmann 2010-03-09 misc tuning
2010-03-09 wenzelm 2010-03-09 Typedecl.typedecl_global;
2010-03-09 wenzelm 2010-03-09 localized typedecl;
2010-03-09 wenzelm 2010-03-09 aliases for class/type/const; tuned;
2010-03-09 wenzelm 2010-03-09 added Name_Space.alias -- additional accesses for an existing entry;
2010-03-09 wenzelm 2010-03-09 merged
2010-03-09 haftmann 2010-03-09 merged
2010-03-09 haftmann 2010-03-09 data administration using canonical functorial operations
2010-03-09 haftmann 2010-03-09 tuned data structures; using AList.map_default
2010-03-09 haftmann 2010-03-09 consistent field names; tuned interface
2010-03-09 haftmann 2010-03-09 weakend class ring_div; tuned
2010-03-09 blanchet 2010-03-09 more work on Nitpick's finite sets
2010-03-09 blanchet 2010-03-09 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
2010-03-09 wenzelm 2010-03-09 ProofContext.read_class/read_type_name_proper;
2010-03-09 wenzelm 2010-03-09 added ProofContext.tsig_of -- proforma version for local name space only, not logical content; added ProofContext.read_type_name_proper; localized ProofContext.read_class/read_arity/cert_arity; localized ProofContext.class_space/type_space etc.;
2010-03-09 wenzelm 2010-03-09 simplified Syntax.basic_syntax (again); separate Syntax.type_ast_trs depending on read_class/read_type;
2010-03-09 wenzelm 2010-03-09 tuned -- eliminated Sign.intern_sort;
2010-03-09 wenzelm 2010-03-09 renamed mk_const_def to legacy_const_def, because of slightly odd Sign.intern_term;
2010-03-09 blanchet 2010-03-09 added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
2010-03-08 huffman 2010-03-08 merged
2010-03-08 huffman 2010-03-08 remove unnecessary error handling code
2010-03-08 huffman 2010-03-08 construct fully typed goal in proof of induction rule
2010-03-08 huffman 2010-03-08 don't generate rule foo.finites for non-flat domains; use take_induct rule to prove induction rule
2010-03-08 huffman 2010-03-08 remove redundant function arguments