2009-06-02 haftmann 2009-06-02 added/moved lemmas by Andreas Lochbihler
2009-06-02 haftmann 2009-06-02 added Fin_Fun theory
2009-06-02 haftmann 2009-06-02 tuned code generator test theories
2009-06-02 haftmann 2009-06-02 OCaml builtin intergers are elusive; avoid
2009-06-02 haftmann 2009-06-02 more aggresive bracketing of let expressions
2009-06-02 haftmann 2009-06-02 tuned whitespace
2009-06-02 wenzelm 2009-06-02 merged
2009-06-02 wenzelm 2009-06-02 merged
2009-06-02 chaieb 2009-06-02 merged
2009-06-02 chaieb 2009-06-02 merged
2009-06-02 chaieb 2009-06-02 merged
2009-06-01 chaieb 2009-06-01 Reverses idempotent; radical of E; generalized logarithm;
2009-06-02 wenzelm 2009-06-02 made SML/NJ happy;
2009-06-02 wenzelm 2009-06-02 merged
2009-06-02 hoelzl 2009-06-02 use algebra_simps instead of ring_simps
2009-06-02 wenzelm 2009-06-02 merged, resolving conflict in src/Pure/Isar/attrib.ML;
2009-06-02 hoelzl 2009-06-02 Generalized Integral_add
2009-06-02 hoelzl 2009-06-02 Added theorems about distinct & concat, map & replicate and concat & replicate
2009-06-02 berghofe 2009-06-02 merged
2009-06-02 berghofe 2009-06-02 Fixed broken code dealing with alternative names.
2009-06-02 berghofe 2009-06-02 Enclosed parts of subsection in @{text ...} to make LaTeX happy.
2009-06-02 berghofe 2009-06-02 Added Convex_Euclidean_Space.thy again.
2009-06-02 haftmann 2009-06-02 made SML/NJ happy
2009-06-01 huffman 2009-06-01 declare Bfun_def [code del]
2009-06-01 huffman 2009-06-01 simp del -> code del
2009-06-01 huffman 2009-06-01 limits of inverse using filters
2009-06-01 huffman 2009-06-01 merged
2009-06-01 huffman 2009-06-01 add [code del] declarations
2009-06-01 huffman 2009-06-01 add dependency on Limits.thy
2009-06-01 nipkow 2009-06-01 new lemma
2009-05-31 huffman 2009-05-31 merged
2009-05-31 huffman 2009-05-31 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
2009-05-31 huffman 2009-05-31 more abstract properties of eventually
2009-05-31 huffman 2009-05-31 new lemmas about eventually; rewrite Lim proofs to use more abstract properties of eventually
2009-05-29 huffman 2009-05-29 generalize at function to class perfect_space
2009-05-29 huffman 2009-05-29 generalize topological notions to class metric_space; add class perfect_space
2009-05-29 huffman 2009-05-29 instance ^ :: (metric_space, finite) metric_space
2009-05-29 huffman 2009-05-29 generalize tendsto and related constants to class metric_space
2009-05-29 huffman 2009-05-29 add lemmas Lim_at_iff_LIM, Lim_sequentially_iff_LIMSEQ
2009-05-29 huffman 2009-05-29 remove duplicate cauchy constant
2009-05-29 huffman 2009-05-29 fix reference to LIM_def
2009-05-29 huffman 2009-05-29 instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
2009-05-29 huffman 2009-05-29 generalize constants from Lim.thy to class metric_space
2009-05-28 huffman 2009-05-28 LIMSEQ_def -> LIMSEQ_iff
2009-05-28 huffman 2009-05-28 generalize constants in SEQ.thy to class metric_space
2009-06-02 wenzelm 2009-06-02 early setup of secure operations (again, cf. deddd77112b7) -- NB: fix_ints is required for bootstrap; late setup of ML_Env and ML_Compiler;
2009-06-01 wenzelm 2009-06-01 structure ML_Compiler;
2009-06-01 wenzelm 2009-06-01 added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
2009-06-01 wenzelm 2009-06-01 added flatten;
2009-06-01 wenzelm 2009-06-01 tuned signature;
2009-06-01 wenzelm 2009-06-01 export secure_mltext;
2009-06-01 wenzelm 2009-06-01 tuned comments;
2009-06-01 wenzelm 2009-06-01 maintain tokens within common ML environment;
2009-06-01 wenzelm 2009-06-01 ML_Env;
2009-06-01 wenzelm 2009-06-01 slightly later setup of ML and secure operations;
2009-06-01 wenzelm 2009-06-01 moved local ML environment to separate module ML_Env;
2009-06-01 wenzelm 2009-06-01 removed print function from global ML name space, to reduce risk of surprises;
2009-06-01 wenzelm 2009-06-01 made SML/NJ happy;
2009-05-31 wenzelm 2009-05-31 attempt to eliminate adhoc makestring at runtime (which is not well-defined);
2009-05-31 wenzelm 2009-05-31 eliminated misleading dummy versions of print/makestring, cf. 6974449ddea9;