isabelle: Graph

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

restructured; circumvent sort problem
2008-12-17, by haftmann
merged.
2008-12-16, by huffman
new theory Dsum: cpo of disjoint sum
2008-12-16, by huffman
scale dependency graph in document
2008-12-16, by huffman
changed the names of insert_eqvt and set_eqvt so that it is clear that they have preconditions
2008-12-16, by Christian Urban
proper document antiquotations;
2008-12-16, by wenzelm
merged
2008-12-16, by wenzelm
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
2008-12-16, by krauss
future proofs: Future.fork_pri 1 minimizes queue length and pending promises
2008-12-16, by wenzelm
renamed structure TaskQueue to Task_Queue;
2008-12-16, by wenzelm
Future.fork_pri;
2008-12-16, by wenzelm
renamed structure TaskQueue to Task_Queue;
2008-12-16, by wenzelm
renamed structure TaskQueue to Task_Queue;
2008-12-16, by wenzelm
renamed structure TaskQueue to Task_Queue;
2008-12-16, by wenzelm
removed old scheduler;
2008-12-16, by wenzelm
tuned enqueue: plain add_edge, acyclic not required here;
2008-12-16, by wenzelm
tuned messages;
2008-12-15, by wenzelm
updated generated file;
2008-12-15, by wenzelm
repaired railroad accident;
2008-12-15, by wenzelm
updated generated files;
2008-12-15, by wenzelm
added 'atp_messages' command, which displays recent messages synchronously;
2008-12-15, by wenzelm
merged
2008-12-15, by nipkow
flipped fold implementation
2008-12-15, by nipkow
merged
2008-12-11, by nipkow
codegen
2008-12-11, by nipkow
code for {x:A. P(x)} and for fold
2008-12-11, by nipkow
Testfile for Stefan's code generator
2008-12-11, by nipkow
moved value.ML to src/Tools
2008-12-15, by haftmann
\underscoreoff is now default
2008-12-15, by haftmann
tuned some proofs
2008-12-15, by Christian Urban
removed Ids;
2008-12-13, by wenzelm
merged
2008-12-13, by berghofe
merged
2008-12-13, by berghofe
merged
2008-12-13, by berghofe
Unified syntax of nominal_primrec with the one used by fun(ction) and new
2008-12-13, by berghofe
Modified nominal_primrec to make it work with local theories, unified syntax
2008-12-13, by berghofe
merged
2008-12-13, by wenzelm
tuned comments;
2008-12-13, by wenzelm
tuned ML_OPTIONS for improved multicore performance;
2008-12-13, by wenzelm
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
2008-12-13, by wenzelm
requires: check ancestors directly;
2008-12-13, by wenzelm
Context.display_names;
2008-12-13, by wenzelm
global_qed: refrain from ProofContext.auto_bind_facts, to avoid
2008-12-12, by wenzelm
usage: echo ML settings as well;
2008-12-13, by wenzelm
future proofs: more robust check via Future.enabled;
2008-12-12, by wenzelm
removed former Isabelle font (cf. IsabelleItalic);
2008-12-11, by wenzelm
incorporated isabelle-fonts side-branch (forced merge);
2008-12-11, by wenzelm
replaced single quote by mathematical prime;
2008-09-06, by wenzelm
generated file;
2008-08-24, by wenzelm
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
instance inat :: semiring_char_0
2008-12-09, by huffman
Default names for definitions.
2008-12-08, by ballarin
Proper shape of assumptions generated from Defines elements.
2008-12-08, by ballarin
Merged.
2008-12-08, by ballarin
Explicitly close up defines.
2008-12-08, by ballarin
Interpretation in proof contexts.
2008-12-05, by ballarin
tuned LaTeX files
2008-12-08, by haftmann
tuned LaTeX files
2008-12-08, by haftmann
merged.
2008-12-06, by huffman
multiplication for type inat
2008-12-06, by huffman
fix proofs
2008-12-06, by huffman