Mercurial
Mercurial
>
repos
>
testboard
/ 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.
fixed use_thy "LocalWeakening";
20070531, by wenzelm
included new example in the compiling process
20070531, by urbanc
a theory using locally nameless terms and strong induction principles
20070531, by urbanc
tuned the proof
20070531, by urbanc
emulate later version of TextIO.inputLine;
20070531, by wenzelm
reversed SML B library patches;
20070531, by wenzelm
TextIO.inputLine: use present SML B library version;
20070531, by wenzelm
tuned USEDIR_OPTIONS;
20070530, by wenzelm
removed HOL4 image, which seldom works;
20070530, by wenzelm
simplified data setup
20070530, by haftmann
instance: always print sorts on failure
20070530, by haftmann
more example
20070530, by haftmann
fixed typo
20070530, by haftmann
updated
20070530, by haftmann
generalized lemmas
20070530, by haftmann
eliminated strings
20070530, by haftmann
tuned
20070530, by haftmann
clarified error message
20070530, by krauss
simplify names of locale interpretations
20070530, by huffman
renamed some lemmas in Complex.thy
20070530, by huffman
cleaned up proofs; reorganized sections; removed redundant lemmas
20070530, by huffman
use newstyle instance declarations
20070529, by huffman
instance complex :: banach
20070529, by huffman
add lemma real_sqrt_sum_squares_less
20070529, by huffman
cleaned up some proofs
20070529, by huffman
interpretation bounded_linear_divide
20070529, by huffman
add bounded_linear lemmas
20070529, by huffman
add isUCont lemmas
20070529, by huffman
updated examples to include an instance of (lexicographic_order simp:...)
20070529, by krauss
Complex: generalized type of exp
20070528, by huffman
generalized exp to work over any complete field; new proof of exp_add
20070528, by huffman
add type annotations for exp
20070528, by huffman
interpretations additive_scaleR_left, additive_scaleR_right
20070528, by huffman
remove division_by_zero requirement from termdiffs lemmas; cleaned up some proofs
20070528, by huffman
new proof of Cauchy product formula for series
20070527, by huffman
What it says
20070526, by nipkow
improved error handling
20070525, by haftmann
using rudimentary class target mechanism
20070525, by haftmann
*** empty log message ***
20070525, by haftmann
fixed typo
20070525, by haftmann
fix typos
20070525, by huffman
*** empty log message ***
20070525, by nipkow
*** empty log message ***
20070525, by nipkow
*** empty log message ***
20070525, by nipkow
tuned
20070525, by nipkow
Added List_Comprehension
20070525, by nipkow
adapted to fix for fresh_fun_simp
20070525, by urbanc
took out Class.thy from the compiling process until memory problems are solved
20070525, by urbanc
simplify some proofs
20070525, by huffman
*** empty log message ***
20070524, by nipkow
Squared things out.
20070524, by obua
fix a bug : the semantics of no_asm was the opposite
20070524, by narboux
temporary fix for a bug in fresh_fun_simp
20070524, by urbanc
formalisation of my PhD (the result was correct, but the proof needed several corrections)
20070524, by urbanc
add an option in fresh_fun_simp to prevent rewriting in assumptions
20070524, by narboux
fixes tvar issue in type inference
20070524, by haftmann
tuned
20070524, by haftmann
tuned warning
20070524, by haftmann
rudimentary class target implementation
20070524, by haftmann
tuned Pure/General/name_space.ML
20070524, by haftmann
less
more

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