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.
tuned signature;
20070414, by wenzelm
read_typ_XXX: no sorts;
20070414, by wenzelm
added read_def_cterms, read_cterm (from thm.ML);
20070414, by wenzelm
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
20070414, by wenzelm
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
20070414, by wenzelm
removed Pure/Syntax/ROOT.ML;
20070414, by wenzelm
Term.string_of_vname;
20070414, by wenzelm
Theory.inferT_axm;
20070414, by wenzelm
do not enable Toplevel.debug globally;
20070414, by wenzelm
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
20070414, by wenzelm
canonical merge operations
20070414, by haftmann
declarations: apply target_morphism;
20070414, by wenzelm
inst(T)_morphism: avoid reference to static theory value;
20070414, by wenzelm
tuned signature;
20070414, by wenzelm
added Morphism.transform/form (generic nonsense);
20070414, by wenzelm
Morphism.transform/form;
20070414, by wenzelm
data declaration: removed obsolete target_morphism (still required for local data!?);
20070414, by wenzelm
data declaration: removed obsolete target_morphism;
20070414, by wenzelm
added eval_antiquotes_fn (tmp);
20070413, by wenzelm
tuned document (headers, sections, spacing);
20070413, by wenzelm
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
less
more

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