isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -300 -100 -14 +14 +100 +300 +1000 +3000 +10000 +30000 tip

renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
2010-04-30, by wenzelm
slightly more standard induct_simp_add/del attributes;
2010-04-30, by wenzelm
map_css: explicitly provide a temporary context, which might be required for mksimps, mkcongs etc.;
2010-04-30, by wenzelm
export Simplifier.with_context;
2010-04-30, by wenzelm
removed some old comments;
2010-04-30, by wenzelm
merged
2010-04-30, by huffman
merged
2010-04-30, by huffman
generalize lemma adjoint_unique; simplify some proofs
2010-04-29, by huffman
fix latex url
2010-04-29, by huffman
merged
2010-04-29, by huffman
define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
2010-04-29, by huffman
remove unused function vector_power, unused lemma one_plus_of_nat_neq_0
2010-04-29, by huffman
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
2010-04-29, by huffman
remove redundant constants pastecart, fstcart, sndcart; users should prefer Pair, fst, snd instead
2010-04-29, by huffman

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -14 +14 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle