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.
adding constants the modern way
20060925, by haftmann
added examples for variable name handling
20060925, by haftmann
better handling for div by zero
20060925, by haftmann
updated theory description
20060925, by haftmann
refinements in codegen serializer
20060925, by haftmann
added 'undefined' serializer
20060925, by haftmann
added code_instname
20060925, by haftmann
reorganized subsection headings
20060924, by huffman
moved SEQ_Infinitesimal from SEQ to HyperNat
20060924, by huffman
real_norm_def [simp]
20060924, by huffman
generalize types of lim and nslim
20060924, by huffman
generalized types of sums, summable, and suminf
20060924, by huffman
add lemma convergent_Cauchy
20060924, by huffman
remove extra dependencies
20060924, by huffman
add proof of summable_LIMSEQ_zero
20060924, by huffman
change definitions from SOME to THE
20060924, by huffman
move root and sqrt stuff from Transcendental to NthRoot
20060924, by huffman
fix proof
20060924, by huffman
added lemmas about LIMSEQ and norm; simplified some proofs
20060922, by huffman
add lemma norm_power
20060922, by huffman
added HOLComplexex;
20060922, by wenzelm
define constants with THE instead of SOME
20060922, by huffman
Fixed bug concerning the generation of identifiers for
20060922, by berghofe
Replaced irreducible_paths by all_paths.
20060922, by berghofe
Added function all_paths (formerly find_paths).
20060922, by berghofe
tuned proofs;
20060922, by wenzelm
tuned oracle name;
20060921, by wenzelm
added is_ml_reserved;
20060921, by wenzelm
member (op =);
20060921, by wenzelm
serial numbers for types;
20060921, by wenzelm
added dest_binop;
20060921, by wenzelm
member (op =);
20060921, by wenzelm
member (op =);
20060921, by wenzelm
tuned eta_contract;
20060921, by wenzelm
added dest_equals_rhs;
20060921, by wenzelm
tuned;
20060921, by wenzelm
serial numbers for consts;
20060921, by wenzelm
Thm.dest_binop;
20060921, by wenzelm
member (op =);
20060921, by wenzelm
member (op =);
20060921, by wenzelm
updated timings;
20060921, by wenzelm
new function hashw_int
20060921, by paulson
Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
20060921, by paulson
corrected for the translation from _ to __ in c_COMBx_e
20060921, by paulson
changed constants into abbreviations; shortened proofs
20060921, by huffman
XML syntax for types, terms, and proofs.
20060921, by berghofe
Added xml_syntax.ML
20060921, by berghofe
Added Tools/xml_syntax.ML
20060921, by berghofe
circumvented defect in SML/NJ type inference
20060921, by haftmann
1. Function package accepts a parameter (default "some_term"), which specifies the functions
20060921, by krauss
removed division_by_zero class requirements from several lemmas
20060921, by huffman
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
20060921, by huffman
choose gnuplot terminal by platform
20060920, by isatest
set terminal png color  works for older versions of gnuplot;
20060920, by wenzelm
added ZFUNITY;
20060920, by wenzelm
tidied
20060920, by paulson
Added in combinator reduction axioms for B' C' and S'. Also split the original reduction axioms into separate files: I+K, B+C, S, B'+C', S'.
20060920, by mengj
make it work on sunbroy2
20060920, by isatest
Moved the functional equality axioms to helper1 files.
20060920, by mengj
Introduced combinators B', C' and S'.
20060920, by mengj
less
more

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