Mon, 08 Mar 2010 15:20:40 -0800 huffman merged
Mon, 08 Mar 2010 14:42:40 -0800 huffman remove unnecessary error handling code
Mon, 08 Mar 2010 14:12:51 -0800 huffman construct fully typed goal in proof of induction rule
Mon, 08 Mar 2010 13:58:00 -0800 huffman don't generate rule foo.finites for non-flat domains; use take_induct rule to prove induction rule
Mon, 08 Mar 2010 12:43:44 -0800 huffman remove redundant function arguments
Mon, 08 Mar 2010 12:36:26 -0800 huffman include take_info within take_induct_info type
Mon, 08 Mar 2010 12:21:07 -0800 huffman pass take_info as an argument to comp_theorems
Mon, 08 Mar 2010 11:58:40 -0800 huffman pass take_induct_info as an argument to comp_theorems
Mon, 08 Mar 2010 11:48:29 -0800 huffman add type take_induct_info
Mon, 08 Mar 2010 11:34:53 -0800 huffman generate take_induct lemmas
Mon, 08 Mar 2010 09:37:03 -0800 huffman move proofs of reach and take lemmas to domain_take_proofs.ML
Mon, 08 Mar 2010 09:33:05 -0800 huffman move lemmas from Domain.thy to Domain_Aux.thy
Mon, 08 Mar 2010 08:12:48 -0800 huffman move take-proofs stuff into new theory Domain_Aux.thy
Mon, 08 Mar 2010 07:37:11 -0800 huffman add type take_info
Mon, 08 Mar 2010 07:22:30 -0800 huffman add function add_qualified_def
Mon, 08 Mar 2010 17:37:09 +0100 haftmann merged
Mon, 08 Mar 2010 14:41:56 +0100 haftmann proper ML interface; further polishing
Mon, 08 Mar 2010 13:22:41 +0100 haftmann code simplification and tuning
Mon, 08 Mar 2010 15:00:34 +0100 berghofe Added inducts field to inductive_result.
Mon, 08 Mar 2010 09:38:59 +0100 haftmann transfer: avoid camel case, more standard coding conventions, misc tuning
Mon, 08 Mar 2010 09:38:58 +0100 haftmann transfer: avoid camel case
Sun, 07 Mar 2010 17:33:01 -0800 huffman merged
Sun, 07 Mar 2010 16:39:31 -0800 huffman generate separate qualified theorem name for each type's reach and take_lemma
Sun, 07 Mar 2010 16:12:01 -0800 huffman add simp rule LAM_strict
Sun, 07 Mar 2010 13:34:53 -0800 huffman fix bug that occurred with 'domain_isomorphism foo = foo * tr * tr'
Sun, 07 Mar 2010 22:36:36 +0100 haftmann merged
Sun, 07 Mar 2010 08:46:12 +0100 haftmann dropped dead code; adhere more closely to standard coding conventions
Sun, 07 Mar 2010 10:03:16 -0800 huffman merged
Sun, 07 Mar 2010 09:57:30 -0800 huffman arith tactic uses 'priority' instead of 'warning' to print messages
Sun, 07 Mar 2010 09:21:16 -0800 huffman add simp rules about Ints, Nats
Sun, 07 Mar 2010 08:40:38 -0800 huffman add more simp rules for Ints
Sun, 07 Mar 2010 07:42:46 -0800 huffman add lemmas Nats_cases and Nats_induct
Sun, 07 Mar 2010 07:29:34 -0800 huffman generalize some lemmas, and remove a few unnecessary ones
Sat, 06 Mar 2010 18:24:30 -0800 huffman generalize some lemmas from class linordered_ring_strict to linordered_ring
Sat, 06 Mar 2010 16:02:22 -0800 huffman add case_names attribute to casedist and ind rules
Sat, 06 Mar 2010 08:08:30 -0800 huffman add some lemmas about complete lattices
Sun, 07 Mar 2010 15:51:29 +0100 wenzelm Digesting strings according to SHA-1.
Sun, 07 Mar 2010 15:49:49 +0100 wenzelm proper int wrapping for Word32;
Sun, 07 Mar 2010 12:47:02 +0100 wenzelm separate structure Typedecl;
Sun, 07 Mar 2010 12:19:47 +0100 wenzelm modernized structure Object_Logic;
Sun, 07 Mar 2010 11:57:16 +0100 wenzelm modernized structure Local_Defs;
Sat, 06 Mar 2010 19:17:59 +0000 paulson merged
Sat, 06 Mar 2010 17:21:59 +0000 paulson merged
Sat, 06 Mar 2010 17:19:29 +0000 paulson simplified
Sat, 06 Mar 2010 20:16:31 +0100 haftmann merged
Sat, 06 Mar 2010 15:31:31 +0100 haftmann lemma restrict_complement_singleton_eq
Sat, 06 Mar 2010 15:31:30 +0100 haftmann some lemma refinements
Sat, 06 Mar 2010 15:31:30 +0100 haftmann added Table.thy
Sat, 06 Mar 2010 17:53:04 +0100 wenzelm provide ProofContext.def_type depending on "pattern" mode;
Sat, 06 Mar 2010 17:32:45 +0100 wenzelm record_type_tr': more robust strip_fields (printed types are not necessarily well-formed, e.g. in Syntax.pretty_arity);
Sat, 06 Mar 2010 16:13:22 +0100 wenzelm record_type_abbr_tr': removed obsolete workaround for decode_type, which now retains syntactic categories of variables vs. constructors (authentic syntax);
Sat, 06 Mar 2010 15:39:16 +0100 wenzelm eliminated Args.bang_facts (legacy feature);
Sat, 06 Mar 2010 15:34:29 +0100 wenzelm eliminated old-style prems;
Sat, 06 Mar 2010 14:35:06 +0100 wenzelm removed unused term_lift_inst_rule (superceded by Subgoal.FOCUS etc.);
Sat, 06 Mar 2010 14:28:31 +0100 wenzelm Some notes on platform support of Isabelle.
Sat, 06 Mar 2010 11:21:09 +0100 haftmann "private" map_of_map lemma
Sat, 06 Mar 2010 09:58:33 +0100 haftmann added insort_insert
Sat, 06 Mar 2010 09:58:30 +0100 haftmann added dom_option_map, map_of_map_keys
Sat, 06 Mar 2010 09:58:28 +0100 haftmann added bulkload; tuned document
Sat, 06 Mar 2010 07:30:21 +0100 haftmann merged
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip