Mercurial
Mercurial
>
repos
>
testboard
/ 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.
do translation: CONST;
20070413, by wenzelm
eval_antiquotes: proper parentheses for projection;
20070413, by wenzelm
canonical merge operations
20070413, by haftmann
Removed erroneous application of rev in get_clauses that caused
20070413, by berghofe
more robust proof
20070413, by krauss
Experimental code for the interpretation of definitions.
20070413, by ballarin
Experimental interpretation code for definitions.
20070413, by ballarin
New file for locale regression tests.
20070413, by ballarin
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
less
more

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