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.
added class Property: basic Isabelle properties;
20080103, by wenzelm
tuned relevance test for presburger
20080103, by chaieb
output message properties: id or position;
20080103, by wenzelm
toplevel print_exn: proper setmp_thread_properties;
20080103, by wenzelm
added id property;
20080103, by wenzelm
Result: added props field;
20080103, by wenzelm
remove legacy ML bindings
20080103, by huffman
newstyle theorem references
20080103, by huffman
fix theorem references
20080103, by huffman
generalized and simplified proof of adm_Finite
20080103, by huffman
new lemma adm_upward
20080103, by huffman
Tuned (type information in Lemmas)
20080103, by chaieb
Changed order of tactics in presburger  thinning before case splits
20080103, by chaieb
maintain thread transition properties;
20080103, by wenzelm
setmp_thread_data;
20080103, by wenzelm
added setmp_thread_data;
20080103, by wenzelm
type transition: added properties field;
20080102, by wenzelm
added properties;
20080102, by wenzelm
Isabelle.command: IsarCmd.nested_command (with properties);
20080102, by wenzelm
added nested_command (with explicit position argument via properties);
20080102, by wenzelm
of_properties: return filtered result;
20080102, by wenzelm
added method encodeProperties;
20080102, by wenzelm
setting H 2000 and no documents for higher performance;
20080102, by wenzelm
add dcpo instance proof
20080102, by huffman
declare upE as cases rule; add new rule up_induct
20080102, by huffman
update sq_ord/po instance proofs
20080102, by huffman
move lemmas from Cont.thy to Ffun.thy;
20080102, by huffman
remove not_up_less_UU [simp]
20080102, by huffman
update instance proofs for sq_ord, po; new instance proofs for dcpo
20080102, by huffman
add lemma ub2ub_monofun'
20080102, by huffman
added dcpo instance proofs
20080102, by huffman
new class dcpo; added dcpo versions of some lemmas
20080102, by huffman
added new lemmas
20080102, by huffman
add lemma dir2dir_monofun
20080102, by huffman
tuned;
20080102, by wenzelm
new is_ub lemmas; new lub syntax for set image
20080102, by huffman
Multithreading.max_threads := 0 refers to number of cores of underlying machine;
20080102, by wenzelm
added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;
20080102, by wenzelm
added usedir M max (alias for M 0);
20080102, by wenzelm
new section for directed sets
20080102, by huffman
split of class uminus
20080102, by haftmann
empty dictionaries for OCaml
20080102, by haftmann
clarified policy
20080102, by haftmann
tuned
20080102, by haftmann
some more antiquotations
20080102, by haftmann
index now a copy of nat rather than int
20080102, by haftmann
absolute import
20080102, by haftmann
some more primrec
20080102, by haftmann
removed some legacy instantiations
20080102, by haftmann
improved evaluation mechanism
20080102, by haftmann
splitted class uminus from class minus
20080102, by haftmann
testing for empty sort
20080102, by paulson
new metis proofs
20080102, by paulson
renamed foldM to fold_mset on general request
20080102, by kleing
update instance proofs to new style
20080102, by huffman
declare sprodE as cases rule; new induction rule sprod_induct
20080101, by huffman
add induction rule ssum_induct
20080101, by huffman
eval_wrapper: CRITICAL;
20080101, by wenzelm
try_ml_file: setmp explicit theory context, prevents race condition wrt. concurrent ML_Context.set_context;
20080101, by wenzelm
tuned spaces;
20080101, by wenzelm
less
more

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