isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

bold version: math glyphs from plain IsabelleMono;
2008-08-24, by wenzelm
fixed rangle;
2008-08-24, by wenzelm
use dash from text font, not math;
2008-08-24, by wenzelm
added glyphs for \<A> (cal), \<a> (rm), \<AA> (\frak), \<aa> (frak);
2008-08-24, by wenzelm
generated ttf;
2008-08-22, by wenzelm
renamed to IsabelleMono;
2008-08-22, by wenzelm
added README with original licenses;
2008-08-22, by wenzelm
renamed Isabelle to IsabelleItalic;
2008-08-22, by wenzelm
fixed rangle glyph;
2008-08-22, by wenzelm
the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
2008-08-22, by wenzelm
Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
2008-08-22, by wenzelm
Isabelle font, based on TeX glyhps;
2008-08-22, by wenzelm
enable future_scheduler by default;
2008-12-11, by wenzelm
ISABELLE_USEDIR_OPTIONS: -M max is default;
2008-12-11, by wenzelm
unified ids for ancestors and checkpoints, removed obsolete history of checkpoints;
2008-12-11, by wenzelm
removed spurious exception_trace;
2008-12-11, by wenzelm
print_theorems: more robust difference, even after finished proof;
2008-12-11, by wenzelm
export context_node;
2008-12-11, by wenzelm
merged
2008-12-11, by wenzelm
more antiquotations;
2008-12-10, by wenzelm
pcpodef package: state two goals, instead of encoded conjunction;
2008-12-11, by wenzelm
recovered goal_pat;
2008-12-11, by wenzelm
inhabitance goal is now stated in original form and result contracted --
2008-12-11, by wenzelm
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
2008-12-11, by wenzelm
add_typedef: unfold set_def in tactical proof as well;
2008-12-11, by wenzelm
merged
2008-12-11, by wenzelm
Theory.checkpoint before commencing proof;
2008-12-11, by wenzelm
misc tuning and modernisation;
2008-12-11, by wenzelm
merged
2008-12-10, by wenzelm
logically separate typedef axiomatization from constant definition
2008-12-08, by krauss
add def before setting up goal
2008-12-08, by krauss
killed dead code
2008-12-07, by krauss
constrain type inference to sort "type"
2008-12-11, by krauss
merged.
2008-12-10, by huffman
cleaned up some proofs in Cfun.thy
2008-12-10, by huffman
implement cont_proc theorem cache using theory data
2008-12-10, by huffman
use ML antiquotations
2008-12-10, by huffman
clean up diff_bin_simps
2008-12-10, by huffman
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
2008-12-10, by huffman
fixed import: requires ContNotDenum;
2008-12-10, by wenzelm
fixed import: requires ContNotDenum;
2008-12-10, by wenzelm
requires RComplete;
2008-12-10, by wenzelm
merged.
2008-12-10, by huffman
move all neg-related lemmas to NatBin; make type of neg specific to int
2008-12-09, by huffman
separate neg_simps from rel_simps
2008-12-09, by huffman
use {less,le}_number_of in integer simprocs
2008-12-09, by huffman
use lemma lists defined in Int.thy
2008-12-09, by huffman
Merged.
2008-12-10, by ballarin
Satisfy a_axioms.
2008-12-10, by ballarin
Merged.
2008-12-10, by ballarin
Enable keyword 'structure' in for clause of locale expression.
2008-12-10, by ballarin
Correct order of defines in specification.
2008-12-09, by ballarin
Pass on defines in inheritance; reject illicit defines created by instantiation.
2008-12-09, by ballarin
Order of implicit parameters in locale expression.
2008-12-09, by ballarin
NewLocale.intro_locales_tac added to Class.default_intro_tac.
2008-12-09, by ballarin
When adding locales, delay notes until local theory is built.
2008-12-09, by ballarin
merged
2008-12-10, by nipkow
moved ContNotDenum into Library
2008-12-10, by nipkow
move lemmas from Numeral_Type.thy to other theories
2008-12-09, by huffman
instantiation option :: (enum) enum
2008-12-09, by huffman

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

isabelle