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.
updated generated document
20090514, by haftmann
merged
20090514, by nipkow
Cleaned up Parity a little
20090514, by nipkow
merged
20090514, by berghofe
merged
20090513, by berghofe
Cleaned up code of function test_term.
20090513, by berghofe
dropped accidental debug messages
20090514, by haftmann
adapted code tutorial to recent changes in code
20090514, by haftmann
more permissive wrt. overloaded constants
20090513, by haftmann
merged
20090513, by haftmann
tuned construction of term_of instances
20090513, by haftmann
tuned construction of term_of instances
20090513, by haftmann
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
less
more

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