Wed, 04 Mar 2009 23:05:32 +0100 wenzelm ML antiquotation @{lemma}: allow 'and' list, proper simultaneous type-checking;
Wed, 04 Mar 2009 19:22:32 +0000 chaieb merged
Wed, 04 Mar 2009 19:21:56 +0000 chaieb Moved general theorems about sums and products to FiniteSet.thy
Wed, 04 Mar 2009 19:21:56 +0000 chaieb fixed proofs; added rules as default simp-rules
Wed, 04 Mar 2009 19:21:56 +0000 chaieb A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
Wed, 04 Mar 2009 19:21:55 +0000 chaieb Added Libray dependency on Topology_Euclidean_Space
Wed, 04 Mar 2009 19:21:55 +0000 chaieb Added general theorems for fold_image, setsum and set_prod
Wed, 04 Mar 2009 19:21:28 +0000 chaieb fixed proofs
Wed, 04 Mar 2009 10:54:47 +0000 chaieb merged
Wed, 04 Mar 2009 10:33:14 +0000 chaieb merged
Wed, 25 Feb 2009 10:29:01 +0000 chaieb merged
Wed, 25 Feb 2009 10:28:49 +0000 chaieb merged
Wed, 04 Mar 2009 18:18:05 +0100 blanchet Second try at adding "nitpick_const_def" attribute.
Wed, 04 Mar 2009 15:49:39 +0100 blanchet Fix parentheses.
Wed, 04 Mar 2009 15:33:07 +0100 blanchet merged
Wed, 04 Mar 2009 15:32:57 +0100 blanchet Added "nitpick_const_simp" attribute to Nominal primrec.
Wed, 04 Mar 2009 14:23:54 +0100 wenzelm NEWS: renamed o2s to Option.set;
Wed, 04 Mar 2009 13:42:23 +0100 haftmann less arbitrary occurrences of undefined
Wed, 04 Mar 2009 13:41:59 +0100 haftmann datatype antiquotation does not assume LaTeX as output any longer
Wed, 04 Mar 2009 11:49:12 +0100 nipkow merged
Wed, 04 Mar 2009 11:48:52 +0100 nipkow Option.thy
Wed, 04 Mar 2009 11:44:05 +0100 haftmann consequent rewrite of index_size, size [index] to nat_of; support pseudo-primrec sepcifications with fun
Wed, 04 Mar 2009 11:37:50 +0100 haftmann merged
Wed, 04 Mar 2009 10:52:47 +0100 haftmann explicit error message for `improper` instances lacking explicit instance parameter constants
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 11:05:02 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:43:39 +0100 blanchet Made Refute.norm_rhs public, so I can use it in Nitpick.
Sun, 01 Mar 2009 18:40:16 +0100 blanchet Added "nitpick_const_def" attribute, for overriding the definition axiom of a constant.
Tue, 24 Feb 2009 16:12:27 +0100 blanchet Eliminated ZCHAFF_VERSION configuration variable, since zChaff's output format is identical in all versions since March 2003 (at least), and also because it forces users who want to use the latest versions to lie about the version number.
Wed, 04 Mar 2009 10:47:35 +0100 nipkow merged
Wed, 04 Mar 2009 10:47:20 +0100 nipkow Made Option a separate theory and renamed option_map to Option.map
Wed, 04 Mar 2009 00:05:20 +0100 wenzelm renamed Method.assumption_tac back to Method.assm_tac -- as assumption_tac it would have to be exactly the tactic behind the assumption method (with facts);
Tue, 03 Mar 2009 21:53:52 +0100 wenzelm eliminated internal stamp equality, replaced by bare-metal pointer_eq;
Tue, 03 Mar 2009 21:49:34 +0100 wenzelm tuned str_of, now subject to verbose flag;
Tue, 03 Mar 2009 21:49:05 +0100 wenzelm added @{binding} ML antiquotations;
Tue, 03 Mar 2009 21:48:40 +0100 wenzelm added print_properties, print_position (again);
Tue, 03 Mar 2009 19:30:43 +0100 wenzelm merged
Tue, 03 Mar 2009 19:21:10 +0100 haftmann merged
Tue, 03 Mar 2009 13:20:53 +0100 haftmann tuned manuals
Tue, 03 Mar 2009 11:00:51 +0100 haftmann more canonical directory structure of manuals
Tue, 03 Mar 2009 18:33:21 +0100 wenzelm merged
Tue, 03 Mar 2009 17:05:18 +0100 nipkow removed and renamed redundant lemmas
Tue, 03 Mar 2009 18:32:01 +0100 wenzelm renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
Tue, 03 Mar 2009 18:31:59 +0100 wenzelm moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
Tue, 03 Mar 2009 17:42:30 +0100 wenzelm added markup for binding;
Tue, 03 Mar 2009 15:12:52 +0100 wenzelm Binding.str_of;
Tue, 03 Mar 2009 15:09:09 +0100 wenzelm Binding.str_of;
Tue, 03 Mar 2009 15:09:08 +0100 wenzelm Binding.str_of;
Tue, 03 Mar 2009 15:09:07 +0100 wenzelm renamed Binding.display to Binding.str_of, which is slightly more canonical;
Tue, 03 Mar 2009 14:54:12 +0100 wenzelm nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;
Tue, 03 Mar 2009 14:53:29 +0100 wenzelm moved name space externalization flags back to name_space.ML;
Tue, 03 Mar 2009 14:52:13 +0100 wenzelm moved name space externalization flags back to name_space.ML;
Tue, 03 Mar 2009 14:16:05 +0100 wenzelm reverted change introduced in a7c164e228e1 -- there cannot be a "bug" in a perfectly normal operation on the internal data representation that merely escaped into public by accident (cf. 0a981c596372);
Tue, 03 Mar 2009 14:08:53 +0100 wenzelm merged
Tue, 03 Mar 2009 14:07:43 +0100 wenzelm Thm.binding;
Tue, 03 Mar 2009 14:07:23 +0100 wenzelm added type binding and val empty_binding;
Tue, 03 Mar 2009 13:22:01 +0100 wenzelm updated generated files;
Tue, 03 Mar 2009 12:12:38 +0100 wenzelm ignore "source" option in antiquotations @{ML}, @{ML_type}, @{ML_struct} -- did not really make sense, without it users can enable source mode globally with less surprises;
Tue, 03 Mar 2009 12:14:52 +1100 Timothy Bourke Implement Makarius's suggestion for improved type pattern parsing.
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip