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.
dropped legacy operations
20090513, by haftmann
tuned construction of typerep instances
20090513, by haftmann
tuned and generalized construction of code equations for eq; tuned interface
20090513, by haftmann
added abstract operations for typerep/term_of
20090513, by haftmann
tuned and generalized construction of code equations for eq
20090513, by haftmann
dropped sort constraint on predicate equality
20090513, by haftmann
itself is instance of eq
20090513, by haftmann
Now deals with division
20090513, by chaieb
updated keywords
20090512, by haftmann
split Predicate_Compile examples into separate theory
20090512, by haftmann
adapted to changes in module Code
20090512, by haftmann
values is now a keyword
20090512, by haftmann
merged
20090512, by haftmann
transferred code generator preprocessor into separate module
20090512, by haftmann
marginally tuned
20090512, by haftmann
examples using code_pred
20090512, by haftmann
added dummy values keyword
20090512, by haftmann
tuned exception code
20090512, by haftmann
A generic arithmetic prover based on Positivstellensatz certificates  also implements FourrierMotzkin elimination as a special case FourrierMotzkin elimination
20090512, by chaieb
A decision method for universal multivariate real arithmetic with add
20090512, by chaieb
Isolated decision procedure for noms and the general arithmetic solver
20090512, by chaieb
Added files Sum_Of_Squares.thy, positivstellensatz.ML and sum_of_squares.ML to Library
20090512, by chaieb
merged
20090511, by huffman
use Pair/fst/snd instead of cpair/cfst/csnd
20090511, by huffman
use Pair/fst/snd instead of cpair/cfst/csnd
20090511, by huffman
move bifinite instance for product type from Cprod.thy to Bifinite.thy
20090511, by huffman
new lemmas
20090511, by huffman
fixed merge accident
20090511, by haftmann
merged
20090511, by haftmann
avoid latex output problem
20090511, by haftmann
merged
20090511, by haftmann
fixed code_pred command
20090511, by bulwahn
Added pred_code command
20090511, by bulwahn
added general preprocessing of equality in predicates for code generation
20090422, by bulwahn
merged
20090511, by haftmann
merged
20090511, by haftmann
mk_number replaces number_of
20090511, by haftmann
qualified names for Lin_Arith tactics and simprocs
20090511, by haftmann
tuned interface of Lin_Arith
20090511, by haftmann
optimized Approximation by precompiling approx_inequality
20090505, by hoelzl
replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
20090429, by hoelzl
merged
20090511, by huffman
newline at end of file
20090511, by huffman
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
20090511, by huffman
removed redundant instance declarations inat :: linorder
20090511, by huffman
merged
20090511, by haftmann
proper error handling for malformed code equations
20090511, by haftmann
corrected deletetion of code equations for constructors
20090511, by haftmann
clarified matter of "proper" flag in code equations
20090511, by haftmann
tuned interface of module Code_Unit
20090511, by haftmann
clarified terminilogy concerning nbe equations
20090511, by haftmann
simplified unoverload/overload policy in code generator preprocessor
20090511, by haftmann
Change to lowercase path names as directed by local pagemasters
20090511, by paulson
merged
20090510, by nipkow
fixed HOLCF proofs
20090510, by nipkow
merged
20090509, by haftmann
interface changes in linarith.ML
20090509, by haftmann
merged
20090509, by nipkow
lemmas by Andreas Lochbihler
20090509, by nipkow
merged
20090508, by nipkow
less
more

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