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.
disable floor_minus and ceiling_minus [simp]
20090226, by huffman
merged
20090226, by wenzelm
merged
20090226, by paulson
Updated the theory syntax. Corrected an error in a command.
20090226, by paulson
merged
20090225, by huffman
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
20090225, by huffman
new theory of Archimedean fields
20090225, by huffman
add lemmas about comparisons of Fract a b with 0 and 1
20090225, by huffman
merged
20090225, by huffman
add lemma diff_Suc_1
20090225, by huffman
Added lemmas for normalizing freshness results involving fresh_star.
20090225, by berghofe
Added typing and evaluation relations, together with proofs of preservation
20090225, by berghofe
merged
20090225, by berghofe
Use LocalTheory.full_name instead of Sign.full_name, because the latter does
20090225, by berghofe
Replaced Logic.unvarify by Variable.import_terms to make declaration of
20090225, by berghofe
nominal_inductive and equivariance now work on local_theory.
20090225, by berghofe
Added equivariance lemmas for fresh_star.
20090225, by berghofe
NEWS
20090225, by nipkow
merged
20090225, by haftmann
robustified
20090225, by haftmann
make more proofs work whether or not One_nat_def is a simp rule
20090224, by huffman
add simp rules for numerals with 1::nat
20090224, by huffman
fix lemma hypreal_hnorm_def
20090224, by huffman
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
20090223, by huffman
move lemma dvd_mod_imp_dvd into class semiring_div
20090223, by huffman
merged
20090223, by haftmann
improved treatment of case certificates
20090223, by haftmann
repaired order of variable node allocation
20090223, by haftmann
explicitly import Fact
20090223, by huffman
change imports to move Fact.thy outside Plain
20090223, by huffman
add lemmas poly_{div,mod}_minus_{left,right}
20090223, by huffman
merged
20090223, by huffman
declare scaleR distrib rules [algebra_simps]; cleaned up
20090222, by huffman
clean up instantiations
20090222, by huffman
merged
20090222, by huffman
simplify some proofs
20090222, by huffman
remove duplicate instance declaration
20090222, by huffman
stripped classrels_of, instances_of
20090223, by haftmann
use canonical subalgebra projection
20090223, by haftmann
experimental switch to new wellsorting algorithm
20090222, by haftmann
handle NONE case in arity function properly
20090222, by haftmann
clarified status of variables in evaluation terms; tuned header
20090222, by haftmann
subalgebra: drop arities if desired
20090222, by haftmann
merged
20090222, by haftmann
more liberality needed
20090222, by haftmann
merged
20090222, by nipkow
added lemmas
20090222, by nipkow
merged
20090222, by haftmann
simplified evaluation
20090222, by haftmann
merged
20090222, by nipkow
added dvd_div_mult
20090222, by nipkow
merged
20090222, by haftmann
first attempt to solve evaluation bootstrap problem
20090222, by haftmann
formal dependency on newly emerging algorithm
20090222, by haftmann
merged
20090222, by nipkow
name fix
20090222, by nipkow
fix spelling
20090221, by huffman
real_inner class instance for vectors
20090221, by huffman
NEWS
20090221, by nipkow
merged
20090221, by nipkow
less
more

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