Wed, 10 Mar 2010 15:58:53 -0800 huffman switch from Nat_Int_Bij to Nat_Bijection
Wed, 10 Mar 2010 15:57:01 -0800 huffman convert HOL-Probability to use Nat_Bijection library
Wed, 10 Mar 2010 15:38:33 -0800 huffman convert SET_Protocol to use Nat_Bijection library
Wed, 10 Mar 2010 15:33:13 -0800 huffman convert TLS to use Nat_Bijection library
Wed, 10 Mar 2010 15:20:13 -0800 huffman adapt HOLCF to use Nat_Bijection library
Wed, 10 Mar 2010 14:57:13 -0800 huffman new theory Library/Nat_Bijection.thy
Wed, 10 Mar 2010 19:21:59 +0100 blanchet improve precision of "card" in Nitpick
Wed, 10 Mar 2010 17:46:28 +0100 blanchet merged
Wed, 10 Mar 2010 16:17:11 +0100 blanchet merged
Wed, 10 Mar 2010 15:06:40 +0100 blanchet show nice error message in Nitpick when "java" is not available
Wed, 10 Mar 2010 14:21:01 +0100 blanchet fixed soundness bug in Nitpick
Wed, 10 Mar 2010 16:40:20 +0100 hoelzl merged
Tue, 09 Mar 2010 16:30:43 +0100 hoelzl Use same order of neq-elimination as in proof search.
Mon, 08 Mar 2010 11:30:55 +0100 hoelzl Moved theorems in Lebesgue to the right places
Wed, 10 Mar 2010 15:29:23 +0100 haftmann constdefs is legacy
Wed, 10 Mar 2010 15:29:22 +0100 haftmann recdef is legacy
Wed, 10 Mar 2010 15:29:22 +0100 haftmann fixed typo
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.
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip