Wed, 10 Mar 2010 15:29:22 +0100 haftmann avoid confusion
Wed, 10 Mar 2010 15:29:21 +0100 haftmann tuned whitespace
Wed, 10 Mar 2010 08:04:50 +0100 haftmann merged
Wed, 10 Mar 2010 08:04:39 +0100 haftmann tuned
Tue, 09 Mar 2010 21:19:49 +0100 haftmann clarified transfer code proper; more natural declaration of return rules
Tue, 09 Mar 2010 21:19:48 +0100 haftmann misc tuning
Tue, 09 Mar 2010 23:32:49 +0100 wenzelm Typedecl.typedecl_global;
Tue, 09 Mar 2010 23:32:13 +0100 wenzelm localized typedecl;
Tue, 09 Mar 2010 23:29:04 +0100 wenzelm aliases for class/type/const;
Tue, 09 Mar 2010 23:27:35 +0100 wenzelm added Name_Space.alias -- additional accesses for an existing entry;
Tue, 09 Mar 2010 20:23:19 +0100 wenzelm merged
Tue, 09 Mar 2010 18:33:01 +0100 haftmann merged
Tue, 09 Mar 2010 18:31:37 +0100 haftmann data administration using canonical functorial operations
Tue, 09 Mar 2010 16:15:19 +0100 haftmann tuned data structures; using AList.map_default
Tue, 09 Mar 2010 15:47:16 +0100 haftmann consistent field names; tuned interface
Tue, 09 Mar 2010 15:47:15 +0100 haftmann weakend class ring_div; tuned
Tue, 09 Mar 2010 16:40:31 +0100 blanchet more work on Nitpick's finite sets
Tue, 09 Mar 2010 14:18:21 +0100 blanchet improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
Tue, 09 Mar 2010 14:36:41 +0100 wenzelm ProofContext.read_class/read_type_name_proper;
Tue, 09 Mar 2010 14:35:02 +0100 wenzelm added ProofContext.tsig_of -- proforma version for local name space only, not logical content;
Tue, 09 Mar 2010 14:29:47 +0100 wenzelm simplified Syntax.basic_syntax (again);
Tue, 09 Mar 2010 14:55:25 +0100 wenzelm tuned -- eliminated Sign.intern_sort;
Tue, 09 Mar 2010 14:18:06 +0100 wenzelm renamed mk_const_def to legacy_const_def, because of slightly odd Sign.intern_term;
Tue, 09 Mar 2010 09:25:23 +0100 blanchet added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
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
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip