Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
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.
debug versions of finite_guess and fresh_guess do not fail if they can not solve the goal
20070413, by narboux
minimize imports
20070413, by huffman
new simp rule exp_ln; new standard proof of DERIV_exp_ln_one; changed imports
20070413, by huffman
moved nonstandard derivative stuff from Deriv.thy into new file HDeriv.thy
20070413, by huffman
added proj_value_antiq;
20070412, by wenzelm
absdummy: use internal name uu to avoid renaming of popular names;
20070412, by wenzelm
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
20070412, by urbanc
updated;
20070412, by wenzelm
output_basic: added isaantiq markup (only inside verbatim tokens);
20070412, by wenzelm
newenvironment{isaantiq};
20070412, by wenzelm
Zero variable indexes in clauses
20070412, by paulson
Improved treatment of classrel/arity clauses
20070412, by paulson
Fixed the treatment of TVars in conjecture clauses (they are deleted, not frozen)
20070412, by paulson
Improved and simplified the treatment of classrel/arity clauses
20070412, by paulson
canonical merge operations
20070412, by haftmann
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
20070412, by huffman
run annomaly from makedist
20070412, by kleing
set special ISABELLE_USER_HOME as in other isatest settings
20070412, by isatest
isatest version of annomaly script. to be run from istatestmakedist.
20070412, by kleing
new standard proof of lemma LIM_inverse
20070412, by huffman
new class syntax for scaleR and norm classes
20070411, by huffman
removed debugging code
20070411, by krauss
canonical merge operations
20070411, by haftmann
tuned
20070411, by haftmann
dropped legacy ML bindings
20070411, by haftmann
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
20070411, by huffman
move lemma real_of_nat_inverse_le_iff from NSA.thy to NthRoot.thy
20070411, by huffman
new standard proof of convergent = Cauchy
20070411, by huffman
new standard proof of LIMSEQ_realpow_zero
20070410, by huffman
new LIM/isCont lemmas for abs, of_real, and power
20070410, by huffman
some restructuring
20070410, by krauss
interpretation bounded_linear_of_real
20070410, by huffman
removed unnecessary premise from power_le_imp_le_base
20070410, by huffman
proper handling of morphisms
20070410, by krauss
Moving "FunDef" up in the HOL development graph, since it is independent from "Recdef" and "Datatype" now.
20070410, by krauss
inline_antiq: no longer forces ML_Syntax.atomic;
20070410, by wenzelm
removed dead code
20070410, by krauss
tuned
20070410, by krauss
added example for definitions in local contexts
20070410, by krauss
removed obsolete workaround
20070410, by krauss
generalized type of lemma setsum_product
20070409, by huffman
new standard proofs of some LIMSEQ lemmas
20070409, by huffman
rearranged sections
20070408, by huffman
remove redundant lemmas
20070408, by huffman
removed obsolete workarounds
20070407, by krauss
deleted remaining instances of swap_simp_a and swap_simp_b (obsolete now)
20070407, by urbanc
tuned slightly the previous commit
20070407, by urbanc
perm_simp can now simplify using the rules (a,b) o a = b and (a,b) o b = a
20070407, by narboux
add new standard proofs for limits of sequences
20070406, by huffman
Replaced add_inductive_i by add_inductive_global.
20070405, by berghofe
 Tried to make name_of_thm more robust against changes of the
20070405, by berghofe
 Removed occurrences of ProofContext.export in add_ind_def that
20070405, by berghofe
thy_deps: sort Context.thy_ord;
20070405, by wenzelm
added thy_ord  order of creation;
20070405, by wenzelm
simplified thy_deps using Theory.ancestors_of (in order of creation);
20070404, by wenzelm
renamed Variable.importT to importT_thms;
20070404, by wenzelm
removed unused dep_graph;
20070404, by wenzelm
theory: maintain ancestors in order of creation;
20070404, by wenzelm
rep_thm/cterm/ctyp: removed obsolete sign field;
20070404, by wenzelm
rebind HOL.refl as refl (hidden by widen.refl);
20070404, by wenzelm
less
more

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