isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip

added lemma
2010-02-18, by nipkow
merged
2010-02-18, by wenzelm
tuned isatest settings;
2010-02-18, by wenzelm
removed unused Theory_Target.begin;
2010-02-18, by wenzelm
locale: more precise treatment of naming vs. binding;
2010-02-18, by wenzelm
Sign.restore_naming -- slightly more robust;
2010-02-18, by wenzelm
typedef: slightly more precise treatment of binding;
2010-02-18, by wenzelm
axclass: more precise treatment of naming vs. binding;
2010-02-18, by wenzelm
more systematic treatment of qualified names derived from binding;
2010-02-18, by wenzelm
pretty_full_theory: proper Syntax.init_pretty_global;
2010-02-18, by wenzelm
made SML/NJ happy (again);
2010-02-18, by wenzelm
merged
2010-02-18, by haftmann
drop code lemma for ordered_keys
2010-02-18, by haftmann
more lemmas about sort(_key)
2010-02-17, by haftmann
added ordered_keys
2010-02-17, by haftmann
isatest: activated HOL-Nitpick_Examples for x86_64-darwin -- should now work with kodkodi-1.2.8;
2010-02-17, by wenzelm
merged
2010-02-17, by blanchet
fix example to reflect change in function signature
2010-02-17, by blanchet
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
2010-02-17, by blanchet
added gotcha to Nitpick manual regarding nonstandard models of "nat"
2010-02-17, by blanchet
improve Nitpick's "Datatypes" rendering for elements containing cycles
2010-02-17, by blanchet
don't destroy "Suc" in Nitpick and fix logic of Kodkod filtering (accidentally flipped in previous change)
2010-02-17, by blanchet
merged
2010-02-17, by blanchet
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
2010-02-17, by blanchet
merge
2010-02-17, by blanchet
reintroduce structural induction hint in Nitpick
2010-02-17, by blanchet
merge
2010-02-17, by blanchet
synchronize Nitpick's wellfoundedness formulas caching
2010-02-17, by blanchet
more work on Nitpick's support for nonstandard models + fix in model reconstruction
2010-02-13, by blanchet
redo Nitpick's nonstandard values as cyclic values (instead of additional constructors)
2010-02-13, by blanchet
minor fixes to Nitpick
2010-02-12, by blanchet
various cosmetic changes to Nitpick
2010-02-12, by blanchet
merged
2010-02-17, by huffman
fix more looping simp rules
2010-02-17, by huffman
remove $ from all HOLCF files
2010-02-17, by huffman
Renamed Multivariate-Analysis/Integration to Multivariate-Analysis/Integration_MV to avoid name clash with Integration.
2010-02-17, by hoelzl
Added integration to Multivariate-Analysis (upto FTC)
2010-02-17, by himmelma
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
2010-02-17, by hoelzl
fix looping simp rule
2010-02-17, by huffman
fix warnings about duplicate simp rules
2010-02-17, by huffman
fix warnings about duplicate simp rules
2010-02-17, by huffman
add theory HOLCF/ex/Strict_Fun.thy
2010-02-17, by huffman
tuned primrec signature: return definienda
2010-02-17, by haftmann
merged
2010-02-17, by haftmann
example for executable choice
2010-02-17, by haftmann
added simple theory about discrete summation
2010-02-17, by haftmann
giving up sunbroy2;
2010-02-17, by wenzelm
merged
2010-02-17, by haftmann
a draft for an example how to turn specifications involving choice executable
2010-02-17, by haftmann
added lemma map_of_map_restrict; generalized lemma dom_const
2010-02-17, by haftmann
adjusted to changes in theory Mapping
2010-02-17, by haftmann
more close integration with theory Map
2010-02-17, by haftmann
mappings implemented by association lists
2010-02-17, by haftmann
merged
2010-02-16, by wenzelm
updated SMT certificates
2010-02-16, by boehmes
include solver arguments as comments in SMT problem files (to distinguish different results from the same problem when caching results)
2010-02-16, by boehmes
updated SMT certificates
2010-02-16, by boehmes
added Cache_IO: cache for output of external tools,
2010-02-16, by boehmes
Rename transp to transpose in HOL-Multivariate_Analysis. (by himmelma)
2010-02-16, by hoelzl
simplified/clarified record print translations;
2010-02-16, by wenzelm
eliminated camel case;
2010-02-16, by wenzelm
tuned;
2010-02-16, by wenzelm
simplified/clarified record translations;
2010-02-16, by wenzelm
moved generic update_name to Pure syntax -- not specific to HOL/record;
2010-02-16, by wenzelm
tuned;
2010-02-16, by wenzelm
comment;
2010-02-16, by wenzelm
conceal internal record definitions;
2010-02-16, by wenzelm
simplified meaning of ProofContext.verbose;
2010-02-16, by wenzelm
refrain from using @{const_name} in syntax translations;
2010-02-16, by wenzelm
misc tuning and simplification;
2010-02-16, by wenzelm
refined and exported record_info;
2010-02-15, by wenzelm
modernized structures;
2010-02-15, by wenzelm
modernized signature -- proper binding;
2010-02-15, by wenzelm
tuned errors;
2010-02-15, by wenzelm
Typedef.the_info;
2010-02-15, by wenzelm
formal markup of constants;
2010-02-15, by wenzelm
tuned document;
2010-02-15, by wenzelm
eliminated old fold;
2010-02-15, by wenzelm
renamed InfixName to Infix etc.;
2010-02-15, by wenzelm
discontinued unnamed infix syntax;
2010-02-15, by wenzelm
eliminated unnamed infixes;
2010-02-15, by wenzelm
apply global morphism for theory, instantiation and overloading target; n.b. target morphism and global morphism coincide for theory target
2010-02-15, by haftmann
clarifed type
2010-02-15, by haftmann
optionally localize assertion labels (based on user-defined offsets) to reduce the effort of label adaptions after changes to the source program
2010-02-14, by boehmes
formal markup of constants;
2010-02-14, by wenzelm
modernized structures;
2010-02-13, by wenzelm
authentic proof syntax;
2010-02-13, by wenzelm
tuned import order
2010-02-12, by haftmann
tuned comments
2010-02-12, by haftmann
merged
2010-02-11, by wenzelm
merged
2010-02-11, by huffman
change generated lemmas dist_eqs and dist_les to iff-style
2010-02-11, by huffman
unfold quantifiers (Ball, Bex, Ex1)
2010-02-11, by boehmes
modernized translations;
2010-02-11, by wenzelm
formal markup of @{syntax_const} and @{const_syntax};
2010-02-11, by wenzelm
modernized translations;
2010-02-11, by wenzelm
numeral syntax: clarify parse trees vs. actual terms;
2010-02-11, by wenzelm
added ML antiquotation @{syntax_const};
2010-02-11, by wenzelm
treat inner token markers as syntax consts;
2010-02-11, by wenzelm
modernized syntax/translations;
2010-02-11, by wenzelm
modernized syntax/translations;
2010-02-11, by wenzelm
modernized translations;
2010-02-11, by wenzelm
merged
2010-02-11, by boehmes
use full paths when importing theories
2010-02-11, by boehmes
merged
2010-02-11, by nipkow
inductive vs inductive_set explanation
2010-02-11, by nipkow
modernized translations;
2010-02-11, by wenzelm
modernized translations;
2010-02-10, by wenzelm
renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;
2010-02-10, by wenzelm
merged
2010-02-10, by berghofe
Fixed bug in code for guessing the name of the variable representing the freshness context.
2010-02-10, by berghofe
dropped last occurence of the linlinordered accident
2010-02-10, by haftmann
dropped Id
2010-02-10, by haftmann
minor metis proof tuning
2010-02-10, by haftmann
merged
2010-02-10, by haftmann
NEWS
2010-02-10, by haftmann
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
2010-02-10, by haftmann
revert uninspired Structure_Syntax experiment
2010-02-10, by haftmann
moved lemma field_le_epsilon from Real.thy to Fields.thy
2010-02-10, by haftmann
merged
2010-02-10, by wenzelm