isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

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

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle