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.
change example to use recursion with continuous function space
20091119, by huffman
add lemma isodefl_cprod
20091119, by huffman
automate definition of map functions; remove unused code
20091119, by huffman
change naming convention for deflation combinators
20091119, by huffman
add new makefile dependencies
20091119, by huffman
prove isomorphism and isodefl rules
20091119, by huffman
avoid using csplit; define copy functions exactly like the current domain package
20091119, by huffman
merged
20091119, by huffman
remove one_typ and tr_typ; add abs/rep lemmas
20091118, by huffman
automate definition of rep/abs functions
20091118, by huffman
get rid of numbers on thy variables
20091118, by huffman
automate proofs of REP equations
20091118, by huffman
cleaned up; factored out fixedpoint definition code
20091118, by huffman
automate solution of domain equations
20091118, by huffman
removed fixme  quickanddirty flag is appropriate
20091120, by Christian Urban
use of thmantiquotation
20091120, by Christian Urban
Added new counterexample generator SML_inductive for goals involving
20091119, by berghofe
Added infrastructure for embedding random data generators into code generated
20091119, by berghofe
unused_thms: show only results from 'theorem(s)' package (via oldstyle kinds);
20091119, by wenzelm
future_result: purge flexflex pairs, which should normally be trivial anyway  prevent Thm.future_result from complaining about tpairs;
20091119, by wenzelm
toplevel pretty printer for Synchronized.var;
20091119, by wenzelm
adapted Local_Theory.define  eliminated odd thm kind;
20091119, by wenzelm
Specification.definition: Thm.definitionK marks exactly the highlevel enduser result;
20091119, by wenzelm
Local_Theory.define: eliminated slightly odd kind argument  such lowlevel definitions should be hardly ever exposed to endusers anyway;
20091119, by wenzelm
merged
20091119, by wenzelm
merged
20091119, by paulson
Minor correction
20091119, by paulson
some attempts to improve termination of isatest;
20091119, by wenzelm
Added the contributions of Robert Himmelmann to CONTRIBUTIONS and NEWS
20091119, by hoelzl
Renamed vector_less_eq_def to the more usual name vector_le_def.
20091119, by hoelzl
merged
20091119, by bulwahn
replacing Predicate_Compile_Preproc_Const_Defs by more general Spec_Rules
20091119, by bulwahn
concealing internal definitions of primrec specifications
20091119, by bulwahn
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
20091119, by bulwahn
changing the proof procedure for parameters; adding a testcase for negation and parameters; adopting print_tac to the latest function print_tac' in the predicate compiler
20091119, by bulwahn
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
20091119, by bulwahn
check if equations are present for all functions to avoid lowlevel exception later
20091119, by krauss
anti_sym > antisym
20091119, by nipkow
optionally trace theorems used in proof reconstruction
20091118, by boehmes
added arithmetic example using div and mod
20091118, by boehmes
bump up Nitpick's axiom/definition unfolding limits, because some realworld problems (e.g. from Boogie) ran into the previous limits;
20091117, by blanchet
merged
20091117, by blanchet
comment out debugging code in Nitpick
20091117, by blanchet
fixed bug in Nitpick's handling of "The" and "Eps" when the return type is a "bool"
20091117, by blanchet
made "NitpickHOL.normalized_rhs_of" more robust in the face of locale definitions
20091117, by blanchet
removed "debug := true" that shouldn't have been submitted in the first place
20091117, by blanchet
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)
20091117, by hoelzl
merged
20091117, by blanchet
run Nitpick examples if Kodkodi is available
20091117, by blanchet
merged
20091117, by wenzelm
fixed "expect" of Nitpick examples to reflect latest changes in Nitpick
20091117, by blanchet
merged
20091117, by blanchet
use SAT solver that's available everywhere for this example
20091117, by blanchet
invoke Kodkodi from Nitpick using new $KODKOD/bin/kodkodi script;
20091117, by blanchet
merged
20091117, by blanchet
added constraint for Eq^ in Nitpick's implementation of the monotonicity calculus
20091116, by blanchet
change the order in which Nitpick tries SAT solvers;
20091116, by blanchet
Fixed splitting of div and mod on integers (split theorem differed from implementation).
20091117, by webertj
merged
20091117, by webertj
Fixed splitting of div and mod on integers (split theorem differed from implementation).
20091117, by webertj
less
more

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