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.
Note about theorem dependencies including themselves.
20050713, by aspinall
Fix informtheoryloaded/retracted > informfileloaded/retracted to match pgip.rnc
20050713, by aspinall
(intermediate commit)
20050713, by haftmann
(corrected wrong commit)
20050713, by haftmann
(intermediate commit)
20050713, by haftmann
 added cplex package to HOL/Matrix
20050713, by obua
avoid some garbage
20050712, by schirmer
 use TableFun instead of homebrew binary tree in am_interpreter.ML
20050712, by obua
 introduce Pure/Tools directory
20050712, by obua
fold_map > fold_yield, added transformator combinators, added selector combinator
20050712, by haftmann
changed orientation of bind_assoc rule
20050712, by huffman
use qualified names for all constants
20050712, by huffman
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
20050712, by huffman
generalized types of monadic operators to class cpo; added match function for UU
20050712, by huffman
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
20050712, by avigad
experimental code to reduce the amount of type information in blast
20050712, by paulson
tweaked
20050712, by paulson
Added \<module> symbol.
20050712, by berghofe
Added "attach" keyword for code generator setup.
20050712, by berghofe
Auxiliary functions to be used in generated code are now defined using "attach".
20050712, by berghofe
Implemented mechanism for attaching auxiliary code to consts_code and
20050712, by berghofe
small text mod
20050711, by nipkow
Fixed some problems with the signal handler.
20050711, by quigley
Improved implementation of Defs.is_overloaded.
20050711, by obua
Some changes to allow mutually recursive, overloaded functions with same name.
20050708, by berghofe
added Davenport reference
20050708, by nipkow
moved Davenport citation to Main, removed author list
20050708, by nipkow
moved gcd to new GCD.thy
20050708, by nipkow
proof needed updating because of arith
20050708, by nipkow
changed imports due to new GCD.thy
20050708, by nipkow
Used to be in Library/Primes
20050708, by nipkow
fix typo
20050708, by huffman
replaced old continuity rules with new lemma cont2cont_lift_case
20050708, by huffman
simplified proof of ifte_thms, removed ifte_simp
20050708, by huffman
renamed upE1 to upE; added simp rule cont2cont_flift1
20050708, by huffman
renamed upE1 to upE
20050708, by huffman
define 'a u with datatype package;
20050708, by huffman
added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
20050708, by huffman
add lemma eq_sprod
20050708, by huffman
add lemma eq_cprod
20050708, by huffman
removed obsolete continuity theorems
20050707, by huffman
define lift type using pcpodef; cleaned up
20050707, by huffman
cleaned up
20050707, by huffman
fixes to work with UU_reorient_simproc
20050707, by huffman
fixes to work with UU_reorient_simproc
20050707, by huffman
fixes to work with UU_reorient_simproc
20050707, by huffman
1) all theorems in Orderings can now be given as a parameter
20050707, by obua
use theorem ch2ch_cont
20050707, by huffman
inserted basic relevancechecking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
20050707, by paulson
updated comment
20050707, by paulson
add UU_reorient_simproc
20050707, by huffman
use theorems ch2ch_cont, cont2contlubE
20050707, by huffman
add lemmas ch2ch_cont and cont2contlubE
20050707, by huffman
Preparations for interpretation of locales in locales.
20050707, by ballarin
takes & in premises apart now.
20050707, by nipkow
linear arithmetic is more powerful now
20050707, by nipkow
linear arithmetic now takes "&" in assumptions apart.
20050707, by nipkow
Used to be part of Finite_Set (or was it SetInterval?)
20050707, by nipkow
fixed antiquotation;
20050706, by wenzelm
removed timers;
20050706, by wenzelm
less
more

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