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.
generalize some lemmas to class t1_space
20100504, by huffman
simplify definition of t1_space; generalize lemma closed_sing and related lemmas
20100504, by huffman
generalize some lemmas
20100504, by huffman
convert comments to 'text' blocks
20100504, by huffman
generalize more lemmas about limits
20100504, by huffman
repaired comments where SOMEthing went utterly wrong (cf. 2b04504fcb69)
20100505, by krauss
merged
20100504, by huffman
generalize types of LIMSEQ and LIM; generalize many lemmas
20100504, by huffman
make (f  a > x) an abbreviation for (f > x) (at a)
20100504, by huffman
make (X > L) an abbreviation for (X > L) sequentially
20100504, by huffman
adapt to removed premise on tendsto lemma (cf. 88f0125c3bd2)
20100504, by huffman
declare cont_discrete_cpo [cont2cont]
20100504, by huffman
remove unneeded constant Zseq
20100503, by huffman
add lemmas eventually_nhds_metric and tendsto_mono
20100503, by huffman
remove unneeded premise
20100503, by huffman
add constants netmap and nhds
20100503, by huffman
Merged.
20100504, by ballarin
Provide internal function for printing a single interpretation.
20100504, by ballarin
Explicitly manage export in dependencies.
20100427, by ballarin
fixed proof (cf. edc381bf7200);
20100504, by wenzelm
Corrected imports; better approximation of dependencies.
20100504, by hoelzl
Add Convex to Library build
20100504, by hoelzl
Removed unnecessary assumption
20100504, by hoelzl
Translating lemmas from Finite_Set to FSet.
20100504, by Cezary Kaliszyk
merged
20100504, by wenzelm
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
less
more

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