2010-02-22 blanchet filter out trivial definitions in Nitpick (e.g. "Topology.topo" from AFP)
2010-02-22 haftmann dropped references to old axclass from documentation
2010-02-22 berghofe Fixed bug that caused (r)trancl_tac to crash when the term denoting the relation
2010-02-22 blanchet fixed a few bugs in Nitpick and removed unreferenced variables
2010-02-22 Cezary Kaliszyk update the keywords files
2010-02-22 Cezary Kaliszyk rename print_maps to print_quotmaps
2010-02-22 haftmann adjusted to cs. 8dfd816713c6
2010-02-22 haftmann NEWS
2010-02-22 haftmann merged
2010-02-22 haftmann tuned proofs
2010-02-22 haftmann ascii syntax for multiset order
2010-02-22 haftmann switched notations for pointwise and multiset order
2010-02-22 haftmann NEWS
2010-02-19 haftmann NEWS
2010-02-19 haftmann merged
2010-02-19 haftmann switched notations for pointwise and multiset order
2010-02-19 haftmann moved remaning class operations from Algebras.thy to Groups.thy
2010-02-19 haftmann hide fact range_def
2010-02-19 haftmann dropped reference to type classes
2010-02-19 haftmann NEWS
2010-02-21 wenzelm filter out authentic const syntax;
2010-02-21 wenzelm slightly more abstract syntax mark/unmark operations;
2010-02-21 wenzelm tuned;
2010-02-21 wenzelm NEWS: authentic syntax for *all* term constants;
2010-02-21 wenzelm concrete syntax for all constructors, to workaround authentic syntax problem with domain package;
2010-02-21 wenzelm adapted to authentic syntax;
2010-02-21 wenzelm adapted to authentic syntax;
2010-02-21 wenzelm adapted to authentic syntax;
2010-02-21 wenzelm authentic syntax for *all* term constants;
2010-02-21 wenzelm binder notation for default print_mode -- to avoid strange output if "xsymbols" is not active;
2010-02-21 wenzelm tuned headers;
2010-02-21 wenzelm simplified syntax -- to make it work for authentic syntax;
2010-02-21 wenzelm modernized notation -- to make it work for authentic syntax;
2010-02-21 wenzelm proper markup of const syntax;
2010-02-20 wenzelm more precise dependencies;
2010-02-20 nipkow added lemma
2010-02-20 nipkow moved reduced Induct/SList back from AFP.
2010-02-20 haftmann adjusted to changes in cs b987b803616d
2010-02-19 wenzelm disabled some old (fragile) isatests;
2010-02-19 wenzelm tuned settings;
2010-02-19 wenzelm fixed document;
2010-02-19 wenzelm eliminated opaque signature matching -- tends to cause problems with toplevel pp for abstract types;
2010-02-19 wenzelm made SML/NJ happy;
2010-02-19 wenzelm tuned;
2010-02-19 wenzelm authentic term syntax;
2010-02-19 wenzelm Thm.def_binding;
2010-02-19 wenzelm moved ancient Drule.get_def to OldGoals.get_def;
2010-02-19 Cezary Kaliszyk quote the constant and theorem name with @{text}
2010-02-19 wenzelm merged
2010-02-19 wenzelm merged
2010-02-19 wenzelm local Simplifier.context;
2010-02-19 wenzelm renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
2010-02-19 wenzelm tuned message;
2010-02-19 wenzelm Lin_Arith.pre_tac: inherit proper simplifier context, and get rid of posthoc renaming of bound variables;
2010-02-19 haftmann merged
2010-02-19 haftmann context theorem is optional
2010-02-19 haftmann added dest_comb
2010-02-19 haftmann a simple concept for datatype invariants
2010-02-19 haftmann using Code.bare_thms_of_cert
2010-02-19 haftmann simplified
2010-02-19 haftmann added code_abstype keyword
2010-02-19 Cezary Kaliszyk Initial version of HOL quotient package.
2010-02-19 blanchet merge
2010-02-18 blanchet added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
2010-02-18 blanchet fix bug in Nitpick's monotonicity code w.r.t. binary integers
2010-02-18 wenzelm merged
2010-02-18 huffman merged
2010-02-18 huffman get rid of many duplicate simp rule warnings
2010-02-18 huffman get rid of warnings about duplicate simp rules in all HOLCF theories
2010-02-18 huffman HOLCF-FOCUS depends on ex/Stream.thy
2010-02-18 huffman fix looping call to simplifier
2010-02-18 berghofe merged
2010-02-18 berghofe Use top-down rewriting to contract abbreviations.
2010-02-18 berghofe Added function rewrite_term_top for top-down rewriting.
2010-02-18 nipkow merged
2010-02-18 nipkow added lemma
2010-02-18 wenzelm merged
2010-02-18 wenzelm tuned isatest settings;
2010-02-18 wenzelm removed unused Theory_Target.begin;
2010-02-18 wenzelm locale: more precise treatment of naming vs. binding;
2010-02-18 wenzelm Sign.restore_naming -- slightly more robust;
2010-02-18 wenzelm typedef: slightly more precise treatment of binding;
2010-02-18 wenzelm axclass: more precise treatment of naming vs. binding;
2010-02-18 wenzelm more systematic treatment of qualified names derived from binding;
2010-02-18 wenzelm pretty_full_theory: proper Syntax.init_pretty_global;
2010-02-18 wenzelm made SML/NJ happy (again);
2010-02-18 haftmann merged
2010-02-18 haftmann drop code lemma for ordered_keys
2010-02-17 haftmann more lemmas about sort(_key)
2010-02-17 haftmann added ordered_keys
2010-02-17 wenzelm isatest: activated HOL-Nitpick_Examples for x86_64-darwin -- should now work with kodkodi-1.2.8;
2010-02-17 blanchet merged
2010-02-17 blanchet fix example to reflect change in function signature
2010-02-17 blanchet make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
2010-02-17 blanchet added gotcha to Nitpick manual regarding nonstandard models of "nat"
2010-02-17 blanchet improve Nitpick's "Datatypes" rendering for elements containing cycles
2010-02-17 blanchet don't destroy "Suc" in Nitpick and fix logic of Kodkod filtering (accidentally flipped in previous change)
2010-02-17 blanchet merged
2010-02-17 blanchet added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
2010-02-17 blanchet merge
2010-02-17 blanchet reintroduce structural induction hint in Nitpick
2010-02-17 blanchet merge
2010-02-17 blanchet synchronize Nitpick's wellfoundedness formulas caching
2010-02-13 blanchet more work on Nitpick's support for nonstandard models + fix in model reconstruction
2010-02-13 blanchet redo Nitpick's nonstandard values as cyclic values (instead of additional constructors)
2010-02-12 blanchet minor fixes to Nitpick
2010-02-12 blanchet various cosmetic changes to Nitpick
2010-02-17 huffman merged
2010-02-17 huffman fix more looping simp rules
2010-02-17 huffman remove $ from all HOLCF files
2010-02-17 hoelzl Renamed Multivariate-Analysis/Integration to Multivariate-Analysis/Integration_MV to avoid name clash with Integration.
2010-02-17 himmelma Added integration to Multivariate-Analysis (upto FTC)
2010-02-17 hoelzl Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
2010-02-17 huffman fix looping simp rule
2010-02-17 huffman fix warnings about duplicate simp rules
2010-02-17 huffman fix warnings about duplicate simp rules
2010-02-17 huffman add theory HOLCF/ex/Strict_Fun.thy
2010-02-17 haftmann tuned primrec signature: return definienda
2010-02-17 haftmann merged
2010-02-17 haftmann example for executable choice
(0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip