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
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.
merged
20120401, by wenzelm
merged
20120401, by krauss
removed old HOL4 import  corresponding exporter is lost, code is broken, no users known, maintenance nightmare
20120401, by krauss
Modernized HOLImport for HOL Light
20120401, by Cezary Kaliszyk
merged
20120401, by wenzelm
adapted Mira configuration to dd04c8173bb2.
20120401, by krauss
removed Nat_Numeral.thy, moving all theorems elsewhere
20120401, by huffman
less brutal return from function, to allow caller to report error;
20120401, by wenzelm
more general context command with auxiliary fixes/assumes etc.;
20120401, by wenzelm
more precise type annotation (cf. 6523a21076a8);
20120401, by wenzelm
nothing specific about named target;
20120401, by wenzelm
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
20120401, by wenzelm
added Attrib.global_notes/local_notes/generic_notes convenience;
20120401, by wenzelm
simplified;
20120401, by wenzelm
tuned signature;
20120401, by wenzelm
clarified Named_Target.target_declaration: propagate through other levels as well;
20120401, by wenzelm
Local_Theory.map_contexts with explicit level indication: 0 = main target at bottom;
20120401, by wenzelm
tuned proofs
20120401, by huffman
merged
20120331, by huffman
tuned proof
20120331, by huffman
add lemma power_le_one
20120331, by huffman
tuned;
20120331, by wenzelm
tuned signature;
20120331, by wenzelm
more direct Local_Defs.contract;
20120331, by wenzelm
more precise Local_Defs.expand wrt. *local* prems only;
20120331, by wenzelm
tuned comment;
20120331, by wenzelm
more robust Scala 2.9.x interpreter invocation  avoid separate interpreter thread and thus deadlock of Swing_Thread.now;
20120330, by wenzelm
tuned;
20120330, by wenzelm
dropped empty files
20120330, by haftmann
dropped now obsolete Cset theories
20120330, by haftmann
merged
20120330, by wenzelm
tuned proofs, less guesswork;
20120330, by wenzelm
merged
20120330, by huffman
load Tools/numeral.ML in Num.thy
20120330, by huffman
tuned proof
20120330, by huffman
set up numeral reorient simproc in Num.thy
20120330, by huffman
remove redundant simp rule
20120330, by huffman
add simp rules for eve/odd on numerals
20120330, by huffman
remove contentfree theory ex/Arithmetic_Series_Complex.thy
20120330, by huffman
rephrase lemmas about arithmetic series using numeral '2'
20120330, by huffman
rephrase lemma card_Pow using '2' instead of 'Suc (Suc 0)'
20120330, by huffman
replace lemmas eval_nat_numeral with a simpler reformulation
20120330, by huffman
restate various simp rules for word operations using pred_numeral
20120330, by huffman
new lemmas for simplifying subtraction on nat numerals
20120330, by huffman
removed redundant natspecific copies of theorems
20120330, by huffman
move more theorems from Nat_Numeral.thy to Num.thy
20120330, by huffman
"invariant" is free in main HOL (cf. 56adbf5bcc82, e64ffc96a49f);
20120330, by wenzelm
more robust ISABELLE_JDK_HOME settings, based on exisiting JAVA_HOME provided by isatest shell environment (which depends a lot on the host);
20120330, by wenzelm
more explicit isatest environment settings (from private .bashrc);
20120330, by wenzelm
merged
20120330, by huffman
fix searchandreplace errors
20120330, by huffman
move lemma card_UNIV_bool from Nat_Numeral.thy to Finite_Set.thy
20120330, by huffman
add constant pred_numeral k = numeral k  (1::nat);
20120330, by huffman
move lemmas from Nat_Numeral.thy to Nat.thy
20120330, by huffman
move lemmas from Nat_Numeral to Int.thy and Num.thy
20120330, by huffman
merged
20120330, by bulwahn
adding theory to prove completeness of the exhaustive generators
20120330, by bulwahn
refine bindings in quickcheck_common: do not conceal and do not declare as simps
20120330, by bulwahn
hiding fact not so aggressively
20120330, by bulwahn
power on predicate relations
20120330, by haftmann
less
more

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