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.
add header
20060926, by huffman
Changed precedence of "op O" (relation composition) from 60 to 75.
20060926, by krauss
handling of \<^const> syntax for case; explicit case names for induction rules for rep_datatype
20060926, by haftmann
tuned syntax for <= <
20060926, by haftmann
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
20060926, by haftmann
renamed 0 and 1 to HOL.zero and HOL.one respectivly
20060926, by haftmann
fixed the definition of "depth"
20060926, by paulson
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
20060926, by paulson
some cleanup
20060925, by haftmann
changed order
20060925, by haftmann
inserted headings
20060925, by haftmann
changed interface in codegen_package.ML
20060925, by haftmann
fixed some mess
20060925, by haftmann
cleaned up
20060925, by haftmann
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
less
more

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