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
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScriptenabled browsers.
tuned LaTeX files
20081208, by haftmann
tuned LaTeX files
20081208, by haftmann
merged.
20081206, by huffman
multiplication for type inat
20081206, by huffman
fix proofs
20081206, by huffman
change lemmas to avoid using neg
20081206, by huffman
simplify less_nat_number_of
20081205, by huffman
add lemma le_nat_number_of
20081205, by huffman
merged
20081206, by wenzelm
adapted to changes in binding module
20081206, by haftmann
merged
20081206, by haftmann
Name.name_of > Binding.base_name
20081205, by haftmann
corrected theory path
20081205, by haftmann
removed Table.extend, NameSpace.extend_table
20081205, by haftmann
renamed force_proof to join_proof;
20081206, by wenzelm
renamed force_proofs to join_proofs;
20081206, by wenzelm
finish_thy: to not collapse checkpoints  allows future proofs to be deferred indefinitely (performance tradeoff: 515% slowdown in sequential batch jobs);
20081206, by wenzelm
improved future_schedule: more robust handling of failed parents (explicit join), final join of all futures, including Exn.release_all;
20081206, by wenzelm
excursion: improve parallelism by not joining proofs here (depends on persistent checkpoints);
20081206, by wenzelm
added new_task;
20081206, by wenzelm
added constant value;
20081206, by wenzelm
refined type deriv: replaced all_promises by max_promise (dependency limit) and open_promises (potentially unfinished/failed promises);
20081205, by wenzelm
uniform treatment of ISABELLE_HOME/contrib vs. ISABELLE_HOME/..;
20081205, by wenzelm
Merged.
20081205, by ballarin
Interpretation in theories including interaction with subclass relation.
20081205, by ballarin
merged
20081205, by haftmann
dropped NameSpace.declare_base
20081205, by haftmann
fix proofs
20081204, by huffman
merged.
20081204, by huffman
revert to using eq_number_of_eq for simplification (Groebner_Examples.thy was broken)
20081204, by huffman
remove duplicated lemmas
20081204, by huffman
include iszero_simps in lemmas comp_arith
20081204, by huffman
add named lemma lists: neg_simps and iszero_simps
20081204, by huffman
change arith_special simps to avoid using neg
20081204, by huffman
merged
20081205, by kleing
run test for sunbroy2 on /tmp,
20081205, by kleing
merged
20081205, by wenzelm
refined Future.fork interfaces, no longer export Future.future;
20081204, by wenzelm
fork/map: no inheritance of group (structure is nested, not parallel);
20081204, by wenzelm
future proofs: pass actual futures to facilitate composite computations;
20081204, by wenzelm
renamed type Lazy.T to lazy;
20081204, by wenzelm
future_scheduler: no global task group, exceptions via collective join;
20081204, by wenzelm
renamed type Lazy.T to lazy;
20081204, by wenzelm
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
20081204, by wenzelm
future proofs: pass actual futures to facilitate composite computations;
20081204, by wenzelm
renamed type Future.T to future;
20081204, by wenzelm
renamed type Lazy.T to lazy;
20081204, by wenzelm
merged.
20081204, by huffman
change more lemmas to avoid using iszero
20081204, by huffman
change some lemmas to avoid using iszero
20081203, by huffman
enable eq_bin_simps for simplifying equalities on numerals
20081203, by huffman
merged
20081204, by haftmann
cleaned up binding module and related code
20081204, by haftmann
NEWS
20081204, by nipkow
fix proofs related to simplification of inequalities on numerals
20081203, by huffman
enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
20081203, by huffman
simplify proof of less_nat_number_of
20081203, by huffman
merged.
20081203, by huffman
fixed proofs due to changes in Int.thy
20081203, by huffman
cleaned up subsection headings;
20081203, by huffman
less
more

(0)
10000
3000
1000
300
100
60
+60
+100
+300
+1000
+3000
+10000
+30000
tip