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
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
tuned proofs;
2012-09-07, by wenzelm
clearer names for functions in Quickcheck's narrowing engine
2012-09-07, by bulwahn
merged
2012-09-07, by nipkow
tuned latex
2012-09-07, by nipkow
lattice instances for option type
2012-09-07, by haftmann
combinator Option.these
2012-09-07, by haftmann
adjusted examples
2012-09-07, by nipkow
countable_datatype method: pre-instantiate induction rule to avoid failure with e.g. datatype a = A "b list" and b = B "a"
2012-09-06, by huffman
handle type constructors not known to be a BNF using the DEADID BNF
2012-09-06, by traytel
respect order of/additional type variables supplied by the user in fixed point constructions;
2012-09-06, by traytel
gracefully handle shadowing case (fourth step of sugar localization)
2012-09-06, by blanchet
careful about constructor types w.r.t. fake context (third step of localization)
2012-09-06, by blanchet
read the real types off the constant types, rather than using the fake parser types (second step of sugar localization)
2012-09-06, by blanchet
tuning
2012-09-06, by blanchet
use "add_type" rather than "add_types_global"
2012-09-06, by blanchet
don't throw away the context when hacking the theory (first step to localize the sugar code)
2012-09-06, by blanchet
tuning
2012-09-06, by blanchet
introduced and used "mk_Freesss", and simplified "mk_Freess(')"
2012-09-06, by blanchet
construct high-level iterator RHS
2012-09-06, by blanchet
option for discarding build results, enabled in particular for Isabelle_makeall
2012-09-06, by krauss
by default, only generate one discriminator for a two-value datatype
2012-09-05, by blanchet
eliminated potentially confusing terminology of Scala "layer";
2012-09-05, by wenzelm
merged
2012-09-05, by wenzelm
tuned proofs;
2012-09-05, by wenzelm
discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
2012-09-05, by wenzelm
honor mixfix specifications
2012-09-05, by blanchet
code indentation
2012-09-05, by blanchet
print timing information
2012-09-05, by blanchet
adapted example
2012-09-05, by blanchet
check type variables on rhs
2012-09-05, by blanchet
proper subsexp projection of Isabelle_Markup.Path, in correspondence to 5d0cd770828e;
2012-09-05, by wenzelm
added tooltip to reveal jEdit platform file name;
2012-09-05, by wenzelm
commented out slow examples again
2012-09-05, by blanchet
fixed (n + 1)st bug in "mk_exhaust_tac" -- arose with uncurried constructors
2012-09-05, by blanchet
fixed "mk_exhaust_tac" for the nth time
2012-09-05, by blanchet
updated README
2012-09-05, by blanchet
ported "Misc_Codata" to new syntax
2012-09-05, by blanchet
ported "Misc_Data" to new syntax
2012-09-05, by blanchet
error message only in case of an error
2012-09-05, by traytel
do not trivialize important internal theorem in quick_and_dirty mode
2012-09-05, by traytel
merged
2012-09-05, by wenzelm
made "mk_case_eq_tac" work in the case where the first constructor is an "alternate" constructor (in which case its discriminator paradoxically starts with a negation)
2012-09-05, by blanchet
tuning (systematic 1-based indices)
2012-09-05, by blanchet
reindented code
2012-09-05, by blanchet
added TODO
2012-09-05, by blanchet
tell "select_prem_tac" not to thin any further premisses -- the "rotate_tac" otherwise confuses it
2012-09-05, by blanchet
fixed "mk_alternate_disc_def_tac" in the case where the constructors are swapped compared with the common Nil/Cons case
2012-09-05, by blanchet
don't get confused by extraneous premisses
2012-09-05, by blanchet
added a check
2012-09-05, by blanchet
NEWS; CONTRIBUTORS
2012-09-04, by Christian Sternagel
misc tuning;
2012-09-05, by wenzelm
no need to wait 3h on macbroy30 (unlike former macbroy6, cf. 6e5b994070c1);
2012-09-05, by wenzelm
more conservative rechecking of processed constraints in subtyping constraint simplification
2012-09-05, by traytel
added comment for Dmitriy
2012-09-05, by blanchet
fixed bug in type instantiation of case theorem
2012-09-05, by blanchet
use empty binding rather than "*" for default
2012-09-05, by blanchet
tuned
2012-09-05, by nipkow
fixed bugs in one-constructor case
2012-09-05, by blanchet
smoothly handle one-constructor types
2012-09-04, by blanchet
fixed some type issues in sugar "exhaust_tac"
2012-09-04, by blanchet
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip