Fri, 06 Mar 2009 14:33:42 +0100 haftmann merged
Fri, 06 Mar 2009 14:33:19 +0100 haftmann added strict_mono predicate
Fri, 06 Mar 2009 11:50:32 +0100 wenzelm Identifiers of some old CVS file versions;
Fri, 06 Mar 2009 11:28:07 +0100 wenzelm recovered generated files;
Fri, 06 Mar 2009 11:25:54 +0100 wenzelm more precise deps;
Fri, 06 Mar 2009 09:35:43 +0100 nipkow merged
Fri, 06 Mar 2009 09:35:29 +0100 nipkow Added Docs
Thu, 05 Mar 2009 23:12:59 +0100 wenzelm render_tree: suppress markup only for empty body (of status messages, cf. da275b7809bd) in order to recover hilite;
Thu, 05 Mar 2009 21:06:59 +0100 wenzelm removed obsolete claset_rules_of, simpset_rules_of -- as proposed in the text;
Thu, 05 Mar 2009 20:55:28 +0100 wenzelm removed unused TableFun().fold_map and GraphFun().fold_map_nodes;
Thu, 05 Mar 2009 20:17:02 +0100 wenzelm removed spurious occurrences of old rep_ss;
Thu, 05 Mar 2009 19:48:02 +0100 wenzelm Thm.add_oracle interface: replaced old bstring by binding;
Thu, 05 Mar 2009 18:19:20 +0100 wenzelm silent chmod;
Thu, 05 Mar 2009 17:35:37 +0100 wenzelm Consts.abbreviate: reject schematic term variables, prevent schematic type variables (hidden polymorphism) via Term.close_schematic_term -- see also 8f84a608883d;
Thu, 05 Mar 2009 17:09:07 +0100 wenzelm close_schematic_term: uniform order of types/terms;
Thu, 05 Mar 2009 15:27:07 +0100 wenzelm eliminated Consts.eq_consts tuning -- this is built into tables and name spaces already;
Thu, 05 Mar 2009 15:25:35 +0100 wenzelm TableFun.join/merge: optimize the important special case where the tables coincide -- NOTE: this changes both the operational behaviour and the result for non-standard join/eq notion;
Thu, 05 Mar 2009 14:29:02 +0100 wenzelm fixed proofs -- follow-up to ecd6f0ca62ea;
Thu, 05 Mar 2009 12:11:25 +0100 wenzelm renamed NameSpace.base to NameSpace.base_name (in accordance with "full_name");
Thu, 05 Mar 2009 12:08:00 +0100 wenzelm renamed NameSpace.base to NameSpace.base_name;
Thu, 05 Mar 2009 11:58:53 +0100 wenzelm eliminated obsolete ProofContext.full_bname;
Thu, 05 Mar 2009 10:54:03 +0100 wenzelm Binding.prefix_of;
Thu, 05 Mar 2009 10:53:49 +0100 wenzelm adapted Binding.dest;
Thu, 05 Mar 2009 10:52:07 +0100 wenzelm added prefix_of;
Thu, 05 Mar 2009 10:19:51 +0100 blanchet Reintroduced previous changes: Made "Refute.norm_rhs" public and simplified the configuration of the BerkMin and zChaff SAT solvers.
Thu, 05 Mar 2009 02:32:46 +0100 wenzelm merged
Wed, 04 Mar 2009 17:12:23 -0800 huffman declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
Thu, 05 Mar 2009 02:27:54 +0100 wenzelm regenerated document;
Thu, 05 Mar 2009 02:24:36 +0100 wenzelm merge with dummy changeset, to recover files in doc-src/IsarImplementation/ which got lost in aea5d7fa7ef5 (potentially due to insensitive file system on Mac OS);
Thu, 05 Mar 2009 02:20:06 +0100 wenzelm dummy changes to produce a new changeset of these files;
Thu, 05 Mar 2009 01:55:38 +0100 wenzelm updated generated file -- changed since @{ML} now ignores source flag;
Thu, 05 Mar 2009 00:16:28 +0100 wenzelm fixed document;
Wed, 04 Mar 2009 23:52:47 +0100 wenzelm removed old/broken CVS Ids;
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.
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip