Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
30000
10000
3000
1000
300
100
50
30
+30
+50
+100
+300
+1000
+3000
+10000
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.
discontinued obsolete Thy_Syntax.report_span  information can be reproduced in Isabelle/Scala;
20110821, by wenzelm
merged
20110821, by wenzelm
replace lemma realpow_two_diff with new lemma square_diff_square_factored
20110820, by huffman
remove redundant lemma real_0_le_divide_iff in favor or zero_le_divide_iff
20110820, by huffman
move lemma add_eq_0_iff to Groups.thy
20110820, by huffman
remove redundant lemma realpow_two_disj, use square_eq_iff or power2_eq_iff instead
20110820, by huffman
rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy
20110820, by huffman
add lemma power2_eq_iff
20110820, by huffman
remove some overspecific rules from the simpset
20110820, by huffman
merged
20110820, by huffman
redefine constant 'trivial_limit' as an abbreviation
20110820, by huffman
purely functional task_queue.ML  moved actual interrupt_unsynchronized to future.ML;
20110821, by wenzelm
refined Task_Queue.cancel: passive tasks are considered running due to pending abort operation;
20110821, by wenzelm
odd workaround for odd problem of load order in HOL/ex/ROOT.ML (!??);
20110820, by wenzelm
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists  order of adjacency is now standardized wrt. Key.ord;
20110820, by wenzelm
clarified get_imports  should not rely on accidental order within graph;
20110820, by wenzelm
tuned Table.delete_safe: avoid potentially expensive attempt of delete;
20110820, by wenzelm
discontinued "Interrupt", which could disturb administrative tasks of the document model;
20110820, by wenzelm
more direct balanced version Ord_List.unions;
20110820, by wenzelm
reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOLProofs)  see also aa9c1e9ef2ce and 4e2abb045eac;
20110820, by wenzelm
tuned future priorities (again);
20110820, by wenzelm
clarified fulfill_norm_proof: no join_thms yet;
20110820, by wenzelm
added Future.joins convenience;
20110820, by wenzelm
merged
20110820, by haftmann
deactivated »unknown« nitpick example
20110820, by haftmann
merged
20110820, by haftmann
tuned proof
20110820, by haftmann
more uniform formatting of specifications
20110820, by haftmann
compatibility layer
20110820, by haftmann
merged
20110820, by haftmann
less
more

(0)
30000
10000
3000
1000
300
100
50
30
+30
+50
+100
+300
+1000
+3000
+10000
tip