2009-06-08 nipkow 2009-06-08 New lemma
2009-06-08 wenzelm 2009-06-08 eliminated hardwired Cygwin setup;
2009-06-08 wenzelm 2009-06-08 Accessing the Cygwin installation.
2009-06-07 wenzelm 2009-06-07 static IsabelleSystem.charset; static IsabelleSystem.is_cygwin -- based on system property "os.name"; smart bootstrapping of Isabelle settings environment (via implicit or explicit ISABELLE_TOOL, or isabelle.tool property, or isabelle via PATH); source_file: removed obsolete special treatment of "ML"; misc tuning and reorganization;
2009-06-07 wenzelm 2009-06-07 isabelle getenv: option -d;
2009-06-06 wenzelm 2009-06-06 no parallel make jobs on macbroy23, which is the machine where SML/XL is tested -- attempt to consume less resources;
2009-06-06 wenzelm 2009-06-06 updated version;
2009-06-07 huffman 2009-06-07 fix type of open
2009-06-07 huffman 2009-06-07 new setL2 lemmas; instance ^ :: (topological_space, finite) topological_space
2009-06-07 huffman 2009-06-07 replace 'topo' with 'open'; add extra type constraint for 'open'
2009-06-07 huffman 2009-06-07 generalize tendsto lemmas for products
2009-06-07 huffman 2009-06-07 move definitions of open, closed to RealVector.thy
2009-06-06 huffman 2009-06-06 lemmas islimptI, islimptE; generalize open_inter_closure_subset
2009-06-06 huffman 2009-06-06 generalize tendsto to class topological_space
2009-06-05 huffman 2009-06-05 put syntax for tendsto in Limits.thy; rename variables
2009-06-08 haftmann 2009-06-08 constant "chars" of all characters
2009-06-08 haftmann 2009-06-08 added infrastructure for definitorial construction of generators for datatypes
2009-06-08 haftmann 2009-06-08 constant "chars" of all characters
2009-06-08 haftmann 2009-06-08 added generator for char and trivial generator for String.literal
2009-06-08 haftmann 2009-06-08 using constant "chars"
2009-06-08 haftmann 2009-06-08 method linarith
2009-06-06 wenzelm 2009-06-06 reraise exceptions to preserve position information;
2009-06-06 wenzelm 2009-06-06 ML_Compiler.exn_message;
2009-06-06 wenzelm 2009-06-06 ML_Compiler.exn_message;
2009-06-06 wenzelm 2009-06-06 added exn_message (formerly in toplevel.ML); eval/code: proper Isar runtime support; tuned signature;
2009-06-06 wenzelm 2009-06-06 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
2009-06-06 wenzelm 2009-06-06 report_parse_tree: ML_open, ML_struct; eval: terminate input by explicit end token, to ensure that Poly/ML attaches proper position to last input token; tuned;
2009-06-06 wenzelm 2009-06-06 export end_pos_of;
2009-06-06 wenzelm 2009-06-06 use: tuned error;
2009-06-06 wenzelm 2009-06-06 added markup ML_open, ML_struct;
2009-06-06 wenzelm 2009-06-06 use_text: pass file name to compiler, tuned;
2009-06-06 wenzelm 2009-06-06 tuned comments;
2009-06-05 wenzelm 2009-06-05 removed obsolete YXML/XML.detect;
2009-06-05 hoelzl 2009-06-05 Approximation: Corrected precision of ln on all real values
2009-06-04 hoelzl 2009-06-04 Approximation: Implemented argument reduction for cosine. Sinus is now implemented in terms of cosine. Sqrt computes on the entire real numbers
2009-06-05 haftmann 2009-06-05 CONTRIBUTORS
2009-06-05 haftmann 2009-06-05 merged
2009-06-05 haftmann 2009-06-05 tuned proofs
2009-06-05 haftmann 2009-06-05 added mk_valtermify_app and mk_random
2009-06-05 haftmann 2009-06-05 Set.insert with authentic syntax
2009-06-05 haftmann 2009-06-05 merged
2009-06-05 haftmann 2009-06-05 Set.insert with authentic syntax
2009-06-04 haftmann 2009-06-04 added trees implementing mappings
2009-06-04 haftmann 2009-06-04 avoid Library.foldl_map
2009-06-04 haftmann 2009-06-04 class replaces axclass
2009-06-04 haftmann 2009-06-04 insert now qualified and with authentic syntax
2009-06-04 haftmann 2009-06-04 lemma about List.foldl and Finite_Set.fold
2009-06-04 haftmann 2009-06-04 dropped legacy ML bindings; tuned
2009-06-04 haftmann 2009-06-04 lemmas about basic set operations and Finite_Set.fold
2009-06-05 nipkow 2009-06-05 merged
2009-06-05 nipkow 2009-06-05 new lemma
2009-06-05 huffman 2009-06-05 merged
2009-06-05 huffman 2009-06-05 fix type of hnorm
2009-06-04 huffman 2009-06-04 define netlimit in terms of eventually
2009-06-04 huffman 2009-06-04 generalize type of 'at' to topological_space; generalize some lemmas
2009-06-04 huffman 2009-06-04 add extra type constraints for dist, norm
2009-06-04 huffman 2009-06-04 generalize norm method to work over class real_normed_vector
2009-06-04 wenzelm 2009-06-04 example settings for Poly/ML 5.3 (experimental);
2009-06-04 wenzelm 2009-06-04 uniform (short) ids on both sides;
2009-06-04 wenzelm 2009-06-04 merged