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 JavaScriptenabled browsers.
convert HOLProbability to use Nat_Bijection library
20100310, by huffman
convert SET_Protocol to use Nat_Bijection library
20100310, by huffman
convert TLS to use Nat_Bijection library
20100310, by huffman
adapt HOLCF to use Nat_Bijection library
20100310, by huffman
new theory Library/Nat_Bijection.thy
20100310, by huffman
improve precision of "card" in Nitpick
20100310, by blanchet
merged
20100310, by blanchet
merged
20100310, by blanchet
show nice error message in Nitpick when "java" is not available
20100310, by blanchet
fixed soundness bug in Nitpick
20100310, by blanchet
merged
20100310, by hoelzl
Use same order of neqelimination as in proof search.
20100309, by hoelzl
Moved theorems in Lebesgue to the right places
20100308, by hoelzl
constdefs is legacy
20100310, by haftmann
recdef is legacy
20100310, by haftmann
fixed typo
20100310, by haftmann
avoid confusion
20100310, by haftmann
tuned whitespace
20100310, by haftmann
merged
20100310, by haftmann
tuned
20100310, by haftmann
clarified transfer code proper; more natural declaration of return rules
20100309, by haftmann
misc tuning
20100309, by haftmann
Typedecl.typedecl_global;
20100309, by wenzelm
localized typedecl;
20100309, by wenzelm
aliases for class/type/const;
20100309, by wenzelm
added Name_Space.alias  additional accesses for an existing entry;
20100309, by wenzelm
merged
20100309, by wenzelm
merged
20100309, by haftmann
data administration using canonical functorial operations
20100309, by haftmann
tuned data structures; using AList.map_default
20100309, by haftmann
consistent field names; tuned interface
20100309, by haftmann
weakend class ring_div; tuned
20100309, by haftmann
more work on Nitpick's finite sets
20100309, by blanchet
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
20100309, by blanchet
ProofContext.read_class/read_type_name_proper;
20100309, by wenzelm
added ProofContext.tsig_of  proforma version for local name space only, not logical content;
20100309, by wenzelm
simplified Syntax.basic_syntax (again);
20100309, by wenzelm
tuned  eliminated Sign.intern_sort;
20100309, by wenzelm
renamed mk_const_def to legacy_const_def, because of slightly odd Sign.intern_term;
20100309, by wenzelm
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
20100309, by blanchet
merged
20100308, by huffman
remove unnecessary error handling code
20100308, by huffman
construct fully typed goal in proof of induction rule
20100308, by huffman
don't generate rule foo.finites for nonflat domains; use take_induct rule to prove induction rule
20100308, by huffman
remove redundant function arguments
20100308, by huffman
include take_info within take_induct_info type
20100308, by huffman
pass take_info as an argument to comp_theorems
20100308, by huffman
pass take_induct_info as an argument to comp_theorems
20100308, by huffman
add type take_induct_info
20100308, by huffman
generate take_induct lemmas
20100308, by huffman
move proofs of reach and take lemmas to domain_take_proofs.ML
20100308, by huffman
move lemmas from Domain.thy to Domain_Aux.thy
20100308, by huffman
move takeproofs stuff into new theory Domain_Aux.thy
20100308, by huffman
add type take_info
20100308, by huffman
add function add_qualified_def
20100308, by huffman
merged
20100308, by haftmann
proper ML interface; further polishing
20100308, by haftmann
code simplification and tuning
20100308, by haftmann
Added inducts field to inductive_result.
20100308, by berghofe
transfer: avoid camel case, more standard coding conventions, misc tuning
20100308, by haftmann
less
more

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