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 JavaScript-enabled browsers.
remove redundant lemmas
2007-05-08, by huffman
fix proof of hypreal_sqrt_sum_squares_ge1
2007-05-08, by huffman
add lemma real_sqrt_sum_squares_triangle_ineq
2007-05-08, by huffman
add lemma abs_norm_cancel
2007-05-08, by huffman
cleaned up
2007-05-08, by huffman
polished some proofs
2007-05-08, by urbanc
add lemmas power2_le_imp_le and power2_less_imp_less
2007-05-08, by huffman
add lemma power_less_imp_less_base
2007-05-08, by huffman
clean up RealVector classes
2007-05-07, by huffman
First-order variant of the fully-typed translation
2007-05-07, by paulson
added further equality example
2007-05-07, by haftmann
changed 'code nofunc' to 'code func del'
2007-05-07, by haftmann
* Context data interfaces;
2007-05-07, by wenzelm
simplified DataFun interfaces: removed name/print, use adhoc value for uninitialized data, init only required for impure data;
2007-05-07, by wenzelm
simplified DataFun interfaces;
2007-05-07, by wenzelm
changed code generator invocation syntax
2007-05-06, by haftmann
PreList imports RecDef
2007-05-06, by haftmann
dropped legacy ML binding
2007-05-06, by haftmann
added auxiliary lemmas for proof tools
2007-05-06, by haftmann
dropped preorders, unified syntax
2007-05-06, by haftmann
minimal import
2007-05-06, by haftmann
dropped HOL.ML
2007-05-06, by haftmann
tuned
2007-05-06, by haftmann
updated Alice version;
2007-05-06, by wenzelm
IntInf.fromInt;
2007-05-06, by wenzelm
added "set" supression
2007-05-06, by nipkow
added test about "set" supression
2007-05-06, by nipkow
polished all proofs and made the theory "self-contained"
2007-05-04, by urbanc
deleted some unnecessary type-annotations
2007-05-03, by urbanc
tuned some of the proofs and added the lemma fresh_bool
2007-05-03, by urbanc
tuned allpairs
2007-05-02, by nipkow
tuned some proofs and changed variable names in some definitions of Nominal.thy
2007-05-02, by urbanc
added allpairs
2007-04-30, by nipkow
removed obsolete get_sg;
2007-04-30, by wenzelm
explicit treatment of legacy_features;
2007-04-30, by wenzelm
Fixing bugs in the partial-typed and fully-typed translations
2007-04-30, by paulson
Removal of dead code
2007-04-30, by paulson
tuned some proofs in CR and properly included CR_Takahashi
2007-04-27, by urbanc
removed obsolete induct/simp tactic;
2007-04-27, by wenzelm
alternative and much simpler proof for Church-Rosser of Beta-Reduction
2007-04-27, by urbanc
use correct email program for sunbroy2
2007-04-27, by kleing
removed legacy ML files;
2007-04-26, by wenzelm
eliminated unnamed infixes;
2007-04-26, by wenzelm
added header;
2007-04-26, by wenzelm
added header;
2007-04-26, by wenzelm
added
2007-04-26, by haftmann
removed lagacy ML files;
2007-04-26, by wenzelm
updated;
2007-04-26, by wenzelm
eliminated unnamed infixes;
2007-04-26, by wenzelm
renamed some old names Theory.xxx to Sign.xxx;
2007-04-26, by wenzelm
eliminated unnamed infixes;
2007-04-26, by wenzelm
added header;
2007-04-26, by wenzelm
eliminated unnamed infixes, tuned syntax;
2007-04-26, by wenzelm
clarified naming policy
2007-04-26, by haftmann
clarified semantics of merge
2007-04-26, by haftmann
moved stuff to Char_nat.thy
2007-04-26, by haftmann
tuned
2007-04-26, by haftmann
slightly tuned
2007-04-26, by haftmann
replaced recdef by function
2007-04-26, by haftmann
cleaned up code generator setup for int
2007-04-26, by haftmann
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip