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;
Sat, 13 Mar 2010 20:33:14 +0100 wenzelm local theory specifications handle hidden polymorphism implicitly;
Sat, 13 Mar 2010 19:35:53 +0100 wenzelm minor tuning and simplification;
Sat, 13 Mar 2010 17:19:12 +0100 wenzelm removed obsolete HOL/Library/Coinductive_List.thy, superceded by thys/Coinductive/Coinductive_List.thy in AFP/f2f5727b77d0;
Sat, 13 Mar 2010 16:44:12 +0100 wenzelm removed old CVS Ids;
Sat, 13 Mar 2010 16:37:15 +0100 wenzelm reverted fe9b43a08187 -- "warning" is a perfectly normal way of tactics to emit spurious messages (although "arith" could be less chatty), while "priority" is a special Proof General protocol message;
Sat, 13 Mar 2010 15:11:59 +0100 wenzelm merged
Fri, 12 Mar 2010 20:04:48 +0100 bulwahn merged
Fri, 12 Mar 2010 14:04:59 +0100 bulwahn adopting predicate compiler to changes in Spec_Rules; removed dependency to Nitpick_Intros
Fri, 12 Mar 2010 12:14:31 +0100 bulwahn adding Spec_Rules to definitional package inductive and inductive_set
Fri, 12 Mar 2010 12:14:30 +0100 bulwahn refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function
Fri, 12 Mar 2010 18:43:22 +0100 nipkow merged
Fri, 12 Mar 2010 18:42:56 +0100 nipkow Reorganized Hoare logic theories; added Hoare_Den
Fri, 12 Mar 2010 16:02:42 +0100 hoelzl merged
Tue, 09 Mar 2010 15:42:23 +0100 himmelma reset smt_certificates
Tue, 09 Mar 2010 15:39:26 +0100 himmelma added lemmas
Fri, 12 Mar 2010 15:48:37 +0100 nipkow merged
Fri, 12 Mar 2010 15:48:18 +0100 nipkow Added Hoare_Op.thy
Fri, 12 Mar 2010 15:35:41 +0100 hoelzl Equality of integral and infinite sum.
Fri, 12 Mar 2010 12:02:22 +0100 blanchet make tests less demanding, to prevent sporadic failures
Sat, 13 Mar 2010 15:12:56 +0100 wenzelm more antiquotations;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip