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.
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
optionally provide extra dead variables to the FP constructions
2012-09-04, by blanchet
merged
2012-09-04, by wenzelm
added robustness
2012-09-04, by blanchet
added build option -R;
2012-09-04, by wenzelm
implemented "mk_case_tac" -- and got rid of "cheat_tac"
2012-09-04, by blanchet
define "case" constant
2012-09-04, by blanchet
renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix
2012-09-04, by blanchet
implemented "mk_half_distinct_tac"
2012-09-04, by blanchet
implemented "mk_inject_tac"
2012-09-04, by blanchet
implemented "mk_exhaust_tac"
2012-09-04, by blanchet
more work on FP sugar
2012-09-04, by blanchet
more work on sugar + simplify Trueprop + eq idiom everywhere
2012-09-04, by blanchet
renamed "disc_exclus" theorem to "disc_exclude"
2012-09-04, by blanchet
more work on FP sugar
2012-09-04, by blanchet
smarter "*" syntax -- fallback on "_" if "*" is impossible
2012-09-04, by blanchet
more work on FP sugar
2012-09-04, by blanchet
renamed theorem
2012-09-04, by blanchet
tuned TODO comment
2012-09-04, by blanchet
allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
2012-09-04, by blanchet
removed oddities
2012-09-04, by blanchet
allow "*" to indicate no discriminator
2012-09-04, by blanchet
tuned TODOs
2012-09-04, by blanchet
started work on sugared "(co)data" commands
2012-09-04, by blanchet
export "wrap" function
2012-09-04, by blanchet
eliminated obsolete "parallel_proofs = 0" restriction (cf. 0e5b859e1c91)
2012-09-04, by traytel
no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
2012-09-04, by traytel
enable parallel terminal proofs in interaction;
2012-09-04, by wenzelm
misc tuning;
2012-09-03, by wenzelm
merged
2012-09-03, by wenzelm
killed internal output
2012-09-03, by traytel
generate coinductive witnesses for codatatypes
2012-09-03, by traytel
generalized signature
2012-09-03, by traytel
added examples for testing of coinductive witnesses
2012-09-03, by traytel
continue with more robust dummy session after failed startup;
2012-09-03, by wenzelm
prefer old startup dialog scheme (cf. 514bb82514df);
2012-09-03, by wenzelm
more permissive handling of plugin startup failure;
2012-09-03, by wenzelm
bypass slow check for inlined files, where it is not really required;
2012-09-03, by wenzelm
more direct access to all-important chunks for text painting;
2012-09-03, by wenzelm
merged
2012-09-03, by nipkow
added annotations after condition in if and while
2012-09-03, by nipkow
merge, resolving trivial conflict;
2012-09-03, by wenzelm
forgot to add lemmas
2012-08-30, by Christian Sternagel
hide newly introduced constant Sublist.sub to allow for name sub in TreeFsetI
2012-08-30, by Christian Sternagel
reverted (accidentally commited) changes from changeset fd4aef9bc7a9
2012-08-30, by Christian Sternagel
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip