Wed, 17 Mar 2010 18:16:31 +0100 blanchet move Sledgehammer files in a directory of their own
Thu, 18 Mar 2010 13:57:00 +0100 haftmann merged
Thu, 18 Mar 2010 13:56:34 +0100 haftmann dropped odd interpretation of comm_monoid_mult into comm_monoid_add
Thu, 18 Mar 2010 13:56:34 +0100 haftmann lemma swap_inj_on, swap_product
Thu, 18 Mar 2010 13:56:33 +0100 haftmann meaningful transfer certificate
Thu, 18 Mar 2010 13:56:33 +0100 haftmann dropped odd interpretation of comm_monoid_mult into comm_monoid_add; consider Min.insert_idem as default simp rule
Thu, 18 Mar 2010 13:56:32 +0100 haftmann updated certificate
Thu, 18 Mar 2010 13:56:32 +0100 haftmann dropped odd interpretation of comm_monoid_mult into comm_monoid_add
Thu, 18 Mar 2010 13:56:32 +0100 haftmann added locales folding_one_(idem); various streamlining and tuning
Thu, 18 Mar 2010 13:56:31 +0100 haftmann generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
Wed, 17 Mar 2010 19:55:07 +0100 boehmes tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
Wed, 17 Mar 2010 17:23:45 +0100 blanchet added one-entry cache around Kodkod invocation
Wed, 17 Mar 2010 16:27:11 +0100 blanchet merged
Wed, 17 Mar 2010 16:26:08 +0100 blanchet solve error in "Nitpick_Mono" + short path when no finite functions are inferred
Wed, 17 Mar 2010 16:11:48 +0100 blanchet minor additions to Nitpick docs
Wed, 17 Mar 2010 08:11:24 -0700 huffman NEWS: Nat_Bijection library
Wed, 17 Mar 2010 12:21:54 +0100 blanchet document "nitpick_choice_spec" attribute
Wed, 17 Mar 2010 12:01:01 +0100 blanchet fix typo in "nitpick_choice_spec" attribute name (singular, not plural)
Wed, 17 Mar 2010 09:14:43 +0100 blanchet added support for "specification" and "ax_specification" constructs to Nitpick
Tue, 16 Mar 2010 08:45:08 +0100 Christian Urban rollback of local typedef until problem with type-variables can be sorted out; fixed header
Tue, 16 Mar 2010 06:55:01 +0100 haftmann adjusted to changes in Finite_Set
Mon, 15 Mar 2010 22:22:28 +0100 wenzelm merged
Mon, 15 Mar 2010 17:34:03 +0100 nipkow merged
Mon, 15 Mar 2010 17:33:41 +0100 nipkow tuned inductions
Mon, 15 Mar 2010 21:59:28 +0100 wenzelm tuned;
Mon, 15 Mar 2010 21:57:35 +0100 wenzelm moved old Sign.intern_term to the place where it is still used;
Mon, 15 Mar 2010 20:27:23 +0100 wenzelm preserve full const name more carefully, and avoid slightly odd Sign.intern_term;
Mon, 15 Mar 2010 18:59:16 +0100 wenzelm replaced type_syntax/term_syntax by uniform syntax_declaration;
Mon, 15 Mar 2010 15:13:22 +0100 haftmann merged
Mon, 15 Mar 2010 15:13:07 +0100 haftmann corrected disastrous syntax declarations
Mon, 15 Mar 2010 13:59:34 +0100 haftmann added stmaryrd for isasymSqinter
Sun, 14 Mar 2010 19:48:33 -0700 huffman use headers consistently
Sun, 14 Mar 2010 19:47:13 -0700 huffman no_document for theory Countable
Sun, 14 Mar 2010 14:10:36 -0700 huffman old domain package also defines map functions
Sun, 14 Mar 2010 14:10:05 -0700 huffman separate map-related code into new function define_map_functions
Sun, 14 Mar 2010 15:50:17 +0100 Christian Urban removed Local_Theory.theory_result by using local Typedef.add_typedef
Sun, 14 Mar 2010 14:36:56 +0100 wenzelm tuned comment;
Sun, 14 Mar 2010 14:31:24 +0100 wenzelm observe standard header format;
Sun, 14 Mar 2010 14:29:30 +0100 wenzelm expose formal text;
Sun, 14 Mar 2010 14:10:21 +0100 wenzelm localized @{class} and @{type};
Sun, 14 Mar 2010 00:51:58 -0800 huffman move functions into holcf_library.ML
Sun, 14 Mar 2010 00:40:04 -0800 huffman simplify definition of when combinators
Sat, 13 Mar 2010 22:00:34 -0800 huffman declare case_names for various induction rules
Sat, 13 Mar 2010 21:07:20 -0800 huffman add case name 'adm' for infinite induction rules
Sat, 13 Mar 2010 20:15:25 -0800 huffman renamed some lemmas generated by the domain package
Sat, 13 Mar 2010 19:06:18 -0800 huffman use Simplifier.context to avoid 'no proof context in simpset' errors from fixrec_simp after theory merge
Sat, 13 Mar 2010 18:16:48 -0800 huffman fixpat command prints legacy_feature warning
Sat, 13 Mar 2010 17:36:53 -0800 huffman merged
Sat, 13 Mar 2010 17:05:34 -0800 huffman pass binding as argument to add_domain_constructors; proper binding for case combinator
Sat, 13 Mar 2010 16:48:57 -0800 huffman pass domain binding as argument to Domain_Theorems.theorems; proper qualified bindings for theorem names
Sat, 13 Mar 2010 15:51:12 -0800 huffman pass take_info as argument to Domain_Theorems.theorems
Sat, 13 Mar 2010 15:18:25 -0800 huffman replace some string arguments with bindings
Sat, 13 Mar 2010 14:30:38 -0800 huffman more consistent use of qualified bindings
Sat, 13 Mar 2010 14:26:26 -0800 huffman avoid unnecessary primed variable names
Sat, 13 Mar 2010 12:24:50 -0800 huffman remove redundant lemmas
Sat, 13 Mar 2010 10:38:38 -0800 huffman fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
Sat, 13 Mar 2010 10:00:45 -0800 huffman fixrec now generates qualified theorem names
Sat, 13 Mar 2010 09:32:19 -0800 huffman no_document for Infinite_Set in HOLCF
Sat, 13 Mar 2010 20:44:12 +0100 wenzelm removed unused Args.maxidx_values and Element.generalize_facts;
Sat, 13 Mar 2010 20:34:22 +0100 wenzelm Local_Theory.define handles hidden polymorphism;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip