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

simple_dialog: allow scala.swing.Component as well;
2010-08-07, by wenzelm
simplified some Markup;
2010-08-07, by wenzelm
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
2010-08-07, by wenzelm
more robust treatment of Markup.token;
2010-08-07, by wenzelm
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
2010-08-07, by wenzelm
concentrate structural document notions in document.scala;
2010-08-07, by wenzelm
maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
2010-08-07, by wenzelm
tuned;
2010-08-07, by wenzelm
more explicit model of pending text edits;
2010-08-07, by wenzelm
more explicit treatment of Swing thread context;
2010-08-07, by wenzelm
replaced individual Document_Model history by all-inclusive one in Session;
2010-08-07, by wenzelm
misc tuning and clarification;
2010-08-07, by wenzelm
avoid null in Scala;
2010-08-06, by wenzelm
updated keywords;
2010-08-06, by wenzelm
removed obsolete Goal.local_future_enforced: Toplevel.run_command is no longer interactive, so Goal.local_future_enabled is sufficient (cf. 349e9223c685 and e07dacec79e7);
2010-08-06, by wenzelm
merged
2010-08-06, by wenzelm
merged
2010-08-06, by blanchet
quotient types registered as codatatypes are no longer quotient types
2010-08-06, by blanchet
added a friendly warning
2010-08-06, by blanchet
extend the scope of limitation about nonconservative extensions
2010-08-06, by blanchet
improved "merge_type_vars" option: map supersorts to subsorts, to avoid distinguishing, say, "{}", and "HOL.type"
2010-08-06, by blanchet
Remove duplicate locale activation code; performance improvement.
2010-08-05, by ballarin
added record field
2010-08-05, by blanchet
added "whack"
2010-08-05, by blanchet
handle "Rep_unit" & Co. gracefully
2010-08-05, by blanchet
added support for "Abs_" and "Rep_" functions on quotient types
2010-08-05, by blanchet
fiddle with specialization etc.
2010-08-05, by blanchet
handle inductive predicates correctly after change in "def" semantics
2010-08-05, by blanchet
don't specialize built-ins or constructors
2010-08-05, by blanchet
more docs
2010-08-05, by blanchet
prevent the expansion of too large definitions -- use equations for these instead
2010-08-05, by blanchet
make nitpick accept "==" for "nitpick_(p)simp"s
2010-08-05, by blanchet
fix bug in Nitpick's "equationalize" function (the prems were ignored) + make it do some basic extensionalization
2010-08-05, by blanchet
deal correctly with Pure.conjunction in mono check
2010-08-05, by blanchet
rename internal functions
2010-08-05, by blanchet
remove buggy and needless condition
2010-08-05, by blanchet
renamed internal function
2010-08-05, by blanchet
Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again;
2010-08-04, by blanchet
avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
2010-08-04, by blanchet
improve datatype symmetry breaking;
2010-08-04, by blanchet
merged
2010-08-04, by blanchet
make SML/NJ happy
2010-08-04, by blanchet
get rid of all "optimizations" regarding "unit" and other cardinality-1 types
2010-08-04, by blanchet
tuning
2010-08-03, by blanchet
better "Pretty" handling
2010-08-03, by blanchet
change formula for enumerating scopes
2010-08-03, by blanchet
example tweaking -- also prevents Nitpick_Tests from using more than 1 thread
2010-08-03, by blanchet
speed up Nitpick examples a little bit
2010-08-03, by blanchet
minor changes
2010-08-03, by blanchet
updated example timings
2010-08-03, by blanchet
more helpful message
2010-08-03, by blanchet
also mention gfp
2010-08-03, by blanchet
bump up the max cardinalities, to use up more of the time given to us by the user
2010-08-03, by blanchet
make tracing monotonicity easier
2010-08-03, by blanchet
more documentation, based on email discussions with a user
2010-08-03, by blanchet
make example easier to parse
2010-08-03, by blanchet
clarify attribute documentation
2010-08-03, by blanchet
choose better example
2010-08-03, by blanchet
fix newly introduced bug w.r.t. conditional equations
2010-08-03, by blanchet
document something I explained in an email to a poweruser
2010-08-03, by blanchet

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

isabelle