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.
merged
20100504, by berghofe
Turned Sem into an inductive definition.
20100504, by berghofe
Corrected handling of "for" parameters.
20100504, by berghofe
induct_true_def and induct_false_def are already contained in induct_rulify_fallback.
20100504, by berghofe
added lemma about irreflexivity of pointer inequality in Imperative_HOL
20100504, by bulwahn
added function ffilter and some lemmas from Finite_Set to the FSet theory
20100504, by bulwahn
merged
20100504, by haftmann
avoid if on rhs of default simp rules
20100504, by haftmann
avoid exception Empty on malformed goal
20100504, by krauss
locale predicates of classes carry a mandatory "class" prefix
20100504, by haftmann
a ring_div is a ring_1_no_zero_divisors
20100504, by haftmann
NEWS
20100504, by haftmann
merged
20100503, by huffman
merged
20100501, by huffman
complete_lattice instance for net type
20100501, by huffman
swap ordering on nets, so x <= y means 'x is finer than y'
20100501, by huffman
fixrec no longer uses global simpset internally to prove equations
20100501, by huffman
move setsum lemmas to Product_plus.thy
20100501, by huffman
remove duplicate lemmas
20100430, by huffman
add lemmas about convergent
20100430, by huffman
Cleanup information theory
20100503, by hoelzl
Moved Convex theory to library.
20100503, by hoelzl
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
20100420, by hoelzl
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
20100504, by wenzelm
simplified/unified fundamental operations on types/terms/proofterms  prefer Same.operation over "option" variant;
20100504, by wenzelm
renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);
20100504, by wenzelm
specification goal: eliminated redundant Thm.legacy_freezeT  the goal is properly declared and should always produce fixed types in the result;
20100504, by wenzelm
UNDISCH/DISJ_CASESL: eliminated slightly odd Thm.legacy_freezeT  these rules appear to be applied to thms with fixed types only;
20100503, by wenzelm
replaced Thm.legacy_freezeT by Thm.unvarify_global  these facts stem from closed definitions, i.e. there are no term Vars;
20100503, by wenzelm
renamed Thm.freezeT to Thm.legacy_freezeT  it is based on Type.legacy_freeze;
20100503, by wenzelm
minor tuning of Thm.strip_shyps  no longer pervasive;
20100503, by wenzelm
simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here;
20100503, by wenzelm
old NEWS on global operations;
20100503, by wenzelm
ProofContext.init_global;
20100503, by wenzelm
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
20100503, by wenzelm
merged
20100503, by haftmann
do not generate code per default  touches file of parent session
20100430, by haftmann
made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)
20100501, by krauss
Backed out changeset 6f11c9b1fb3e (breaks compilation of HOL image)
20100501, by krauss
now if this doesn't make SML/NJ happy, nothing will
20100501, by blanchet
more stats;
20100501, by wenzelm
renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
20100430, by wenzelm
slightly more standard induct_simp_add/del attributes;
20100430, by wenzelm
map_css: explicitly provide a temporary context, which might be required for mksimps, mkcongs etc.;
20100430, by wenzelm
export Simplifier.with_context;
20100430, by wenzelm
removed some old comments;
20100430, by wenzelm
merged
20100430, by huffman
merged
20100430, by huffman
generalize lemma adjoint_unique; simplify some proofs
20100429, by huffman
fix latex url
20100429, by huffman
merged
20100429, 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
20100429, by huffman
remove unused function vector_power, unused lemma one_plus_of_nat_neq_0
20100429, by huffman
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
20100429, by huffman
remove redundant constants pastecart, fstcart, sndcart; users should prefer Pair, fst, snd instead
20100429, by huffman
generalize LIMSEQ_vector to tendsto_vector
20100428, by huffman
generalize orthogonal_clauses
20100428, by huffman
remove redundant lemma vector_dist_norm
20100428, by huffman
remove redundant lemma norm_0
20100428, by huffman
generalize some euclidean space lemmas
20100428, by huffman
less
more

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