| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
|
changeset |
files
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
enabling a previously broken example of the predicate compiler again
|
changeset |
files
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
improving handling of case expressions in predicate rewriting
|
changeset |
files
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
adding depth_limited_random compilation to predicate compiler
|
changeset |
files
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
a new simpler random compilation for the predicate compiler
|
changeset |
files
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
reviving the classical depth-limited computation in the predicate compiler
|
changeset |
files
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
cleaning the function flattening
|
changeset |
files
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
generalized split transformation in the function flattening
|
changeset |
files
|
| Mon, 22 Mar 2010 08:30:12 +0100 |
bulwahn |
only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
|
changeset |
files
|
| Mon, 22 Mar 2010 08:30:12 +0100 |
bulwahn |
restructuring function flattening
|
changeset |
files
|
| Mon, 22 Mar 2010 08:30:12 +0100 |
bulwahn |
renaming mk_prems to flatten in the function flattening
|
changeset |
files
|
| Mon, 22 Mar 2010 08:30:12 +0100 |
bulwahn |
simplifying function flattening
|
changeset |
files
|
| Mon, 22 Mar 2010 11:45:09 +0100 |
boehmes |
removed warning_count (known causes for warnings have been resolved)
|
changeset |
files
|
| Mon, 22 Mar 2010 10:38:28 +0100 |
blanchet |
remove the iteration counter from Sledgehammer's minimizer
|
changeset |
files
|
| Mon, 22 Mar 2010 10:25:44 +0100 |
blanchet |
merged
|
changeset |
files
|
| Mon, 22 Mar 2010 10:25:07 +0100 |
blanchet |
start work on direct proof reconstruction for Sledgehammer
|
changeset |
files
|
| Fri, 19 Mar 2010 16:04:15 +0100 |
blanchet |
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
|
changeset |
files
|
| Fri, 19 Mar 2010 15:33:18 +0100 |
blanchet |
move all ATP setup code into ATP_Wrapper
|
changeset |
files
|
| Fri, 19 Mar 2010 15:07:44 +0100 |
blanchet |
move the Sledgehammer Isar commands together into one file;
|
changeset |
files
|
| Fri, 19 Mar 2010 13:02:18 +0100 |
blanchet |
more Sledgehammer refactoring
|
changeset |
files
|
| Mon, 22 Mar 2010 09:54:22 +0100 |
boehmes |
use a proof context instead of a local theory
|
changeset |
files
|
| Mon, 22 Mar 2010 09:46:04 +0100 |
boehmes |
provide a hook to safely manipulate verification conditions
|
changeset |
files
|
| Mon, 22 Mar 2010 09:40:11 +0100 |
boehmes |
replaced old-style Drule.add_axiom by Specification.axiomatization
|
changeset |
files
|
| Mon, 22 Mar 2010 09:39:10 +0100 |
boehmes |
removed e-mail address from error message
|
changeset |
files
|
| Mon, 22 Mar 2010 09:32:28 +0100 |
haftmann |
merged
|
changeset |
files
|
| Sun, 21 Mar 2010 08:46:50 +0100 |
haftmann |
tuned whitespace
|
changeset |
files
|
| Sun, 21 Mar 2010 08:46:49 +0100 |
haftmann |
handle hidden polymorphism in class target (without class target syntax, though)
|
changeset |
files
|
| Mon, 22 Mar 2010 00:51:18 +0100 |
wenzelm |
replaced Theory.add_axioms(_i) by more primitive Theory.add_axiom;
|
changeset |
files
|
| Mon, 22 Mar 2010 00:48:56 +0100 |
wenzelm |
replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;
|
changeset |
files
|
| Sun, 21 Mar 2010 22:24:04 +0100 |
wenzelm |
add_axiom: axiomatize "unconstrained" version, with explicit of_class premises;
|
changeset |
files
|
| Sun, 21 Mar 2010 22:13:31 +0100 |
wenzelm |
Logic.mk_of_sort convenience;
|
changeset |
files
|
| Sun, 21 Mar 2010 19:30:19 +0100 |
wenzelm |
more explicit invented name;
|
changeset |
files
|
| Sun, 21 Mar 2010 19:28:25 +0100 |
wenzelm |
minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization';
|
changeset |
files
|
| Sun, 21 Mar 2010 19:04:46 +0100 |
wenzelm |
do not open ML structures;
|
changeset |
files
|
| Sun, 21 Mar 2010 17:28:35 +0100 |
wenzelm |
modernized overloaded definitions;
|
changeset |
files
|
| Sun, 21 Mar 2010 17:12:31 +0100 |
wenzelm |
standard headers;
|
changeset |
files
|
| Sun, 21 Mar 2010 16:51:37 +0100 |
wenzelm |
slightly more uniform definitions -- eliminated old-style meta-equality;
|
changeset |
files
|
| Sun, 21 Mar 2010 15:57:40 +0100 |
wenzelm |
eliminated old constdefs;
|
changeset |
files
|
| Sun, 21 Mar 2010 06:59:23 +0100 |
haftmann |
corrected setup for of_list
|
changeset |
files
|
| Sat, 20 Mar 2010 17:33:11 +0100 |
wenzelm |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
changeset |
files
|
| Sat, 20 Mar 2010 02:23:41 +0100 |
Christian Urban |
added lemma infinite_Un
|
changeset |
files
|
| Fri, 19 Mar 2010 06:14:37 +0100 |
Cezary Kaliszyk |
Check that argument is not a 'Bound' before calling fastype_of.
|
changeset |
files
|
| Fri, 19 Mar 2010 00:47:23 +0100 |
wenzelm |
typedef etc.: no constraints;
|
changeset |
files
|
| Fri, 19 Mar 2010 00:46:08 +0100 |
wenzelm |
allow sort constraints in HOL/typedef;
|
changeset |
files
|
| Fri, 19 Mar 2010 00:43:49 +0100 |
wenzelm |
allow sort constraints in HOL/typedef and related HOLCF variants;
|
changeset |
files
|
| Fri, 19 Mar 2010 00:42:17 +0100 |
wenzelm |
OuterParse.type_args_constrained;
|
changeset |
files
|
| Fri, 19 Mar 2010 00:41:34 +0100 |
wenzelm |
support type arguments with sort constraints;
|
changeset |
files
|
| Thu, 18 Mar 2010 23:08:52 +0100 |
wenzelm |
typedecl: no sort constraints;
|
changeset |
files
|
| Thu, 18 Mar 2010 23:00:18 +0100 |
wenzelm |
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints;
|
changeset |
files
|
| Thu, 18 Mar 2010 22:59:44 +0100 |
wenzelm |
typedecl: no sort constraints;
|
changeset |
files
|
| Thu, 18 Mar 2010 22:56:32 +0100 |
wenzelm |
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
|
changeset |
files
|
| Tue, 16 Mar 2010 16:27:28 +0100 |
hoelzl |
Added product measure space
|
changeset |
files
|
| Thu, 18 Mar 2010 14:52:11 +0100 |
blanchet |
added type constraints to make SML/NJ happy
|
changeset |
files
|
| Thu, 18 Mar 2010 13:59:20 +0100 |
blanchet |
merged
|
changeset |
files
|
| Thu, 18 Mar 2010 13:43:50 +0100 |
blanchet |
fix Mirabelle after renaming Sledgehammer structures
|
changeset |
files
|
| Thu, 18 Mar 2010 13:14:54 +0100 |
blanchet |
merged
|
changeset |
files
|
| Thu, 18 Mar 2010 12:58:52 +0100 |
blanchet |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
changeset |
files
|
| Wed, 17 Mar 2010 19:37:44 +0100 |
blanchet |
renamed "ATP_Linkup" theory to "Sledgehammer"
|
changeset |
files
|
| Wed, 17 Mar 2010 19:26:05 +0100 |
blanchet |
renamed Sledgehammer structures
|
changeset |
files
|
| Wed, 17 Mar 2010 18:16:31 +0100 |
blanchet |
move Sledgehammer files in a directory of their own
|
changeset |
files
|
| Thu, 18 Mar 2010 13:57:00 +0100 |
haftmann |
merged
|
changeset |
files
|
| Thu, 18 Mar 2010 13:56:34 +0100 |
haftmann |
dropped odd interpretation of comm_monoid_mult into comm_monoid_add
|
changeset |
files
|
| Thu, 18 Mar 2010 13:56:34 +0100 |
haftmann |
lemma swap_inj_on, swap_product
|
changeset |
files
|
| Thu, 18 Mar 2010 13:56:33 +0100 |
haftmann |
meaningful transfer certificate
|
changeset |
files
|
| 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
|
changeset |
files
|
| Thu, 18 Mar 2010 13:56:32 +0100 |
haftmann |
updated certificate
|
changeset |
files
|
| Thu, 18 Mar 2010 13:56:32 +0100 |
haftmann |
dropped odd interpretation of comm_monoid_mult into comm_monoid_add
|
changeset |
files
|
| Thu, 18 Mar 2010 13:56:32 +0100 |
haftmann |
added locales folding_one_(idem); various streamlining and tuning
|
changeset |
files
|
| 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
|
changeset |
files
|
| Wed, 17 Mar 2010 19:55:07 +0100 |
boehmes |
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
|
changeset |
files
|
| Wed, 17 Mar 2010 17:23:45 +0100 |
blanchet |
added one-entry cache around Kodkod invocation
|
changeset |
files
|
| Wed, 17 Mar 2010 16:27:11 +0100 |
blanchet |
merged
|
changeset |
files
|
| Wed, 17 Mar 2010 16:26:08 +0100 |
blanchet |
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
|
changeset |
files
|
| Wed, 17 Mar 2010 16:11:48 +0100 |
blanchet |
minor additions to Nitpick docs
|
changeset |
files
|
| Wed, 17 Mar 2010 08:11:24 -0700 |
huffman |
NEWS: Nat_Bijection library
|
changeset |
files
|
| Wed, 17 Mar 2010 12:21:54 +0100 |
blanchet |
document "nitpick_choice_spec" attribute
|
changeset |
files
|
| Wed, 17 Mar 2010 12:01:01 +0100 |
blanchet |
fix typo in "nitpick_choice_spec" attribute name (singular, not plural)
|
changeset |
files
|
| Wed, 17 Mar 2010 09:14:43 +0100 |
blanchet |
added support for "specification" and "ax_specification" constructs to Nitpick
|
changeset |
files
|
| 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
|
changeset |
files
|
| Tue, 16 Mar 2010 06:55:01 +0100 |
haftmann |
adjusted to changes in Finite_Set
|
changeset |
files
|
| Mon, 15 Mar 2010 22:22:28 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 15 Mar 2010 17:34:03 +0100 |
nipkow |
merged
|
changeset |
files
|
| Mon, 15 Mar 2010 17:33:41 +0100 |
nipkow |
tuned inductions
|
changeset |
files
|
| Mon, 15 Mar 2010 21:59:28 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 15 Mar 2010 21:57:35 +0100 |
wenzelm |
moved old Sign.intern_term to the place where it is still used;
|
changeset |
files
|
| Mon, 15 Mar 2010 20:27:23 +0100 |
wenzelm |
preserve full const name more carefully, and avoid slightly odd Sign.intern_term;
|
changeset |
files
|
| Mon, 15 Mar 2010 18:59:16 +0100 |
wenzelm |
replaced type_syntax/term_syntax by uniform syntax_declaration;
|
changeset |
files
|
| Mon, 15 Mar 2010 15:13:22 +0100 |
haftmann |
merged
|
changeset |
files
|
| Mon, 15 Mar 2010 15:13:07 +0100 |
haftmann |
corrected disastrous syntax declarations
|
changeset |
files
|
| Mon, 15 Mar 2010 13:59:34 +0100 |
haftmann |
added stmaryrd for isasymSqinter
|
changeset |
files
|
| Sun, 14 Mar 2010 19:48:33 -0700 |
huffman |
use headers consistently
|
changeset |
files
|
| Sun, 14 Mar 2010 19:47:13 -0700 |
huffman |
no_document for theory Countable
|
changeset |
files
|
| Sun, 14 Mar 2010 14:10:36 -0700 |
huffman |
old domain package also defines map functions
|
changeset |
files
|
| Sun, 14 Mar 2010 14:10:05 -0700 |
huffman |
separate map-related code into new function define_map_functions
|
changeset |
files
|
| Sun, 14 Mar 2010 15:50:17 +0100 |
Christian Urban |
removed Local_Theory.theory_result by using local Typedef.add_typedef
|
changeset |
files
|
| Sun, 14 Mar 2010 14:36:56 +0100 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Sun, 14 Mar 2010 14:31:24 +0100 |
wenzelm |
observe standard header format;
|
changeset |
files
|
| Sun, 14 Mar 2010 14:29:30 +0100 |
wenzelm |
expose formal text;
|
changeset |
files
|
| Sun, 14 Mar 2010 14:10:21 +0100 |
wenzelm |
localized @{class} and @{type};
|
changeset |
files
|
| Sun, 14 Mar 2010 00:51:58 -0800 |
huffman |
move functions into holcf_library.ML
|
changeset |
files
|
| Sun, 14 Mar 2010 00:40:04 -0800 |
huffman |
simplify definition of when combinators
|
changeset |
files
|
| Sat, 13 Mar 2010 22:00:34 -0800 |
huffman |
declare case_names for various induction rules
|
changeset |
files
|
| Sat, 13 Mar 2010 21:07:20 -0800 |
huffman |
add case name 'adm' for infinite induction rules
|
changeset |
files
|
| Sat, 13 Mar 2010 20:15:25 -0800 |
huffman |
renamed some lemmas generated by the domain package
|
changeset |
files
|
| 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
|
changeset |
files
|
| Sat, 13 Mar 2010 18:16:48 -0800 |
huffman |
fixpat command prints legacy_feature warning
|
changeset |
files
|
| Sat, 13 Mar 2010 17:36:53 -0800 |
huffman |
merged
|
changeset |
files
|
| Sat, 13 Mar 2010 17:05:34 -0800 |
huffman |
pass binding as argument to add_domain_constructors; proper binding for case combinator
|
changeset |
files
|
| Sat, 13 Mar 2010 16:48:57 -0800 |
huffman |
pass domain binding as argument to Domain_Theorems.theorems; proper qualified bindings for theorem names
|
changeset |
files
|
| Sat, 13 Mar 2010 15:51:12 -0800 |
huffman |
pass take_info as argument to Domain_Theorems.theorems
|
changeset |
files
|
| Sat, 13 Mar 2010 15:18:25 -0800 |
huffman |
replace some string arguments with bindings
|
changeset |
files
|
| Sat, 13 Mar 2010 14:30:38 -0800 |
huffman |
more consistent use of qualified bindings
|
changeset |
files
|
| Sat, 13 Mar 2010 14:26:26 -0800 |
huffman |
avoid unnecessary primed variable names
|
changeset |
files
|
| Sat, 13 Mar 2010 12:24:50 -0800 |
huffman |
remove redundant lemmas
|
changeset |
files
|
| 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
|
changeset |
files
|
| Sat, 13 Mar 2010 10:00:45 -0800 |
huffman |
fixrec now generates qualified theorem names
|
changeset |
files
|
| Sat, 13 Mar 2010 09:32:19 -0800 |
huffman |
no_document for Infinite_Set in HOLCF
|
changeset |
files
|
| Sat, 13 Mar 2010 20:44:12 +0100 |
wenzelm |
removed unused Args.maxidx_values and Element.generalize_facts;
|
changeset |
files
|
| Sat, 13 Mar 2010 20:34:22 +0100 |
wenzelm |
Local_Theory.define handles hidden polymorphism;
|
changeset |
files
|
| Sat, 13 Mar 2010 20:33:14 +0100 |
wenzelm |
local theory specifications handle hidden polymorphism implicitly;
|
changeset |
files
|
| Sat, 13 Mar 2010 19:35:53 +0100 |
wenzelm |
minor tuning and simplification;
|
changeset |
files
|
| 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;
|
changeset |
files
|
| Sat, 13 Mar 2010 16:44:12 +0100 |
wenzelm |
removed old CVS Ids;
|
changeset |
files
|
| 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;
|
changeset |
files
|
| Sat, 13 Mar 2010 15:11:59 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 12 Mar 2010 20:04:48 +0100 |
bulwahn |
merged
|
changeset |
files
|
| Fri, 12 Mar 2010 14:04:59 +0100 |
bulwahn |
adopting predicate compiler to changes in Spec_Rules; removed dependency to Nitpick_Intros
|
changeset |
files
|
| Fri, 12 Mar 2010 12:14:31 +0100 |
bulwahn |
adding Spec_Rules to definitional package inductive and inductive_set
|
changeset |
files
|
| Fri, 12 Mar 2010 12:14:30 +0100 |
bulwahn |
refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function
|
changeset |
files
|
| Fri, 12 Mar 2010 18:43:22 +0100 |
nipkow |
merged
|
changeset |
files
|
| Fri, 12 Mar 2010 18:42:56 +0100 |
nipkow |
Reorganized Hoare logic theories; added Hoare_Den
|
changeset |
files
|
| Fri, 12 Mar 2010 16:02:42 +0100 |
hoelzl |
merged
|
changeset |
files
|
| Tue, 09 Mar 2010 15:42:23 +0100 |
himmelma |
reset smt_certificates
|
changeset |
files
|
| Tue, 09 Mar 2010 15:39:26 +0100 |
himmelma |
added lemmas
|
changeset |
files
|
| Fri, 12 Mar 2010 15:48:37 +0100 |
nipkow |
merged
|
changeset |
files
|
| Fri, 12 Mar 2010 15:48:18 +0100 |
nipkow |
Added Hoare_Op.thy
|
changeset |
files
|
| Fri, 12 Mar 2010 15:35:41 +0100 |
hoelzl |
Equality of integral and infinite sum.
|
changeset |
files
|
| Fri, 12 Mar 2010 12:02:22 +0100 |
blanchet |
make tests less demanding, to prevent sporadic failures
|
changeset |
files
|
| Sat, 13 Mar 2010 15:12:56 +0100 |
wenzelm |
more antiquotations;
|
changeset |
files
|
| Sat, 13 Mar 2010 15:12:47 +0100 |
wenzelm |
command 'typedef' now works within a local theory context;
|
changeset |
files
|
| Sat, 13 Mar 2010 15:12:17 +0100 |
wenzelm |
removed obsolete HOL 'typedecl';
|
changeset |
files
|
| Sat, 13 Mar 2010 14:44:47 +0100 |
wenzelm |
adapted to localized typedef: handle single global interpretation only;
|
changeset |
files
|
| Sat, 13 Mar 2010 14:43:04 +0100 |
wenzelm |
global typedef;
|
changeset |
files
|
| Sat, 13 Mar 2010 14:42:16 +0100 |
wenzelm |
localized typedef;
|
changeset |
files
|
| Sat, 13 Mar 2010 14:41:37 +0100 |
wenzelm |
added typedecl_wrt, which affects default sorts of type args;
|
changeset |
files
|
| Sat, 13 Mar 2010 14:41:14 +0100 |
wenzelm |
Local_Defs.contract convenience;
|
changeset |
files
|
| Sat, 13 Mar 2010 14:40:36 +0100 |
wenzelm |
added Local_Theory.alias operations (independent of target);
|
changeset |
files
|
| Thu, 11 Mar 2010 23:47:16 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 11 Mar 2010 19:06:03 +0100 |
nipkow |
merged
|
changeset |
files
|
| Thu, 11 Mar 2010 19:05:46 +0100 |
nipkow |
converted proofs to Isar
|
changeset |
files
|
| Thu, 11 Mar 2010 17:52:15 +0100 |
haftmann |
merged
|
changeset |
files
|
| Thu, 11 Mar 2010 17:39:45 +0100 |
haftmann |
merged
|
changeset |
files
|
| Thu, 11 Mar 2010 15:52:35 +0100 |
haftmann |
tuned prefix of ac rules
|
changeset |
files
|
| Thu, 11 Mar 2010 15:52:35 +0100 |
haftmann |
deleted default simp rule card.insert
|
changeset |
files
|
| Thu, 11 Mar 2010 15:52:34 +0100 |
haftmann |
updated generated certificate
|
changeset |
files
|
| Thu, 11 Mar 2010 15:52:34 +0100 |
haftmann |
replaced card_def by card_eq_setsum
|
changeset |
files
|
| Thu, 11 Mar 2010 15:52:33 +0100 |
haftmann |
NEWS
|
changeset |
files
|
| Thu, 11 Mar 2010 14:40:29 +0100 |
haftmann |
Big_Operators now in Main rather than Plain
|
changeset |
files
|
| Thu, 11 Mar 2010 14:39:58 +0100 |
haftmann |
tuned prefixes of ac interpretations
|
changeset |
files
|
| Thu, 11 Mar 2010 14:39:58 +0100 |
haftmann |
Big_Operators now in Main rather than Plain src/HOL/Wellfounded.thy
|
changeset |
files
|
| Thu, 11 Mar 2010 14:38:20 +0100 |
haftmann |
fixed typo
|
changeset |
files
|
| Thu, 11 Mar 2010 14:38:19 +0100 |
haftmann |
tuned monoid locales and prefix of sublocale interpretations
|
changeset |
files
|
| Thu, 11 Mar 2010 14:38:13 +0100 |
haftmann |
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
|
changeset |
files
|
| Thu, 11 Mar 2010 14:38:09 +0100 |
haftmann |
fixed typo
|
changeset |
files
|
| Wed, 10 Mar 2010 16:53:43 +0100 |
haftmann |
added locales for monoids
|
changeset |
files
|
| Wed, 10 Mar 2010 16:53:27 +0100 |
haftmann |
split off theory Big_Operators from theory Finite_Set
|
changeset |
files
|
| Thu, 11 Mar 2010 17:48:07 +0100 |
blanchet |
moved some Nitpick code around
|
changeset |
files
|
| Thu, 11 Mar 2010 23:45:41 +0100 |
wenzelm |
more basic Local_Defs.export_cterm;
|
changeset |
files
|
| Thu, 11 Mar 2010 23:07:12 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 11 Mar 2010 23:07:02 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 11 Mar 2010 18:52:50 +0100 |
wenzelm |
actually apply morphism to binding;
|
changeset |
files
|
| Thu, 11 Mar 2010 16:56:22 +0100 |
wenzelm |
absolute lib_path relative to ML_HOME -- for improved robustness;
|
changeset |
files
|
| Thu, 11 Mar 2010 15:33:45 +0100 |
blanchet |
added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
|
changeset |
files
|
| Thu, 11 Mar 2010 12:22:11 +0100 |
blanchet |
added term postprocessor to Nitpick, to provide custom syntax for typedefs
|
changeset |
files
|
| Thu, 11 Mar 2010 10:13:24 +0100 |
blanchet |
made "Manual_Nits" tests more robust
|
changeset |
files
|
| Thu, 11 Mar 2010 09:09:51 +0100 |
haftmann |
merged
|
changeset |
files
|
| Thu, 11 Mar 2010 09:09:43 +0100 |
haftmann |
made smlnj happy
|
changeset |
files
|
| Wed, 10 Mar 2010 16:06:48 -0800 |
huffman |
replace Nat_Int_Bij with Nat_Bijection in ROOT.ML
|
changeset |
files
|
| Wed, 10 Mar 2010 16:00:51 -0800 |
huffman |
remove obsolete theory Nat_Int_Bij
|
changeset |
files
|
| Wed, 10 Mar 2010 15:58:53 -0800 |
huffman |
switch from Nat_Int_Bij to Nat_Bijection
|
changeset |
files
|
| Wed, 10 Mar 2010 15:57:01 -0800 |
huffman |
convert HOL-Probability to use Nat_Bijection library
|
changeset |
files
|
| Wed, 10 Mar 2010 15:38:33 -0800 |
huffman |
convert SET_Protocol to use Nat_Bijection library
|
changeset |
files
|
| Wed, 10 Mar 2010 15:33:13 -0800 |
huffman |
convert TLS to use Nat_Bijection library
|
changeset |
files
|
| Wed, 10 Mar 2010 15:20:13 -0800 |
huffman |
adapt HOLCF to use Nat_Bijection library
|
changeset |
files
|
| Wed, 10 Mar 2010 14:57:13 -0800 |
huffman |
new theory Library/Nat_Bijection.thy
|
changeset |
files
|
| Wed, 10 Mar 2010 19:21:59 +0100 |
blanchet |
improve precision of "card" in Nitpick
|
changeset |
files
|
| Wed, 10 Mar 2010 17:46:28 +0100 |
blanchet |
merged
|
changeset |
files
|
| Wed, 10 Mar 2010 16:17:11 +0100 |
blanchet |
merged
|
changeset |
files
|
| Wed, 10 Mar 2010 15:06:40 +0100 |
blanchet |
show nice error message in Nitpick when "java" is not available
|
changeset |
files
|
| Wed, 10 Mar 2010 14:21:01 +0100 |
blanchet |
fixed soundness bug in Nitpick
|
changeset |
files
|
| Wed, 10 Mar 2010 16:40:20 +0100 |
hoelzl |
merged
|
changeset |
files
|
| Tue, 09 Mar 2010 16:30:43 +0100 |
hoelzl |
Use same order of neq-elimination as in proof search.
|
changeset |
files
|
| Mon, 08 Mar 2010 11:30:55 +0100 |
hoelzl |
Moved theorems in Lebesgue to the right places
|
changeset |
files
|
| Wed, 10 Mar 2010 15:29:23 +0100 |
haftmann |
constdefs is legacy
|
changeset |
files
|
| Wed, 10 Mar 2010 15:29:22 +0100 |
haftmann |
recdef is legacy
|
changeset |
files
|
| Wed, 10 Mar 2010 15:29:22 +0100 |
haftmann |
fixed typo
|
changeset |
files
|
| Wed, 10 Mar 2010 15:29:22 +0100 |
haftmann |
avoid confusion
|
changeset |
files
|
| Wed, 10 Mar 2010 15:29:21 +0100 |
haftmann |
tuned whitespace
|
changeset |
files
|
| Wed, 10 Mar 2010 08:04:50 +0100 |
haftmann |
merged
|
changeset |
files
|
| Wed, 10 Mar 2010 08:04:39 +0100 |
haftmann |
tuned
|
changeset |
files
|
| Tue, 09 Mar 2010 21:19:49 +0100 |
haftmann |
clarified transfer code proper; more natural declaration of return rules
|
changeset |
files
|
| Tue, 09 Mar 2010 21:19:48 +0100 |
haftmann |
misc tuning
|
changeset |
files
|
| Tue, 09 Mar 2010 23:32:49 +0100 |
wenzelm |
Typedecl.typedecl_global;
|
changeset |
files
|
| Tue, 09 Mar 2010 23:32:13 +0100 |
wenzelm |
localized typedecl;
|
changeset |
files
|
| Tue, 09 Mar 2010 23:29:04 +0100 |
wenzelm |
aliases for class/type/const;
|
changeset |
files
|
| Tue, 09 Mar 2010 23:27:35 +0100 |
wenzelm |
added Name_Space.alias -- additional accesses for an existing entry;
|
changeset |
files
|
| Tue, 09 Mar 2010 20:23:19 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 09 Mar 2010 18:33:01 +0100 |
haftmann |
merged
|
changeset |
files
|
| Tue, 09 Mar 2010 18:31:37 +0100 |
haftmann |
data administration using canonical functorial operations
|
changeset |
files
|
| Tue, 09 Mar 2010 16:15:19 +0100 |
haftmann |
tuned data structures; using AList.map_default
|
changeset |
files
|
| Tue, 09 Mar 2010 15:47:16 +0100 |
haftmann |
consistent field names; tuned interface
|
changeset |
files
|
| Tue, 09 Mar 2010 15:47:15 +0100 |
haftmann |
weakend class ring_div; tuned
|
changeset |
files
|
| Tue, 09 Mar 2010 16:40:31 +0100 |
blanchet |
more work on Nitpick's finite sets
|
changeset |
files
|
| 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"
|
changeset |
files
|
| Tue, 09 Mar 2010 14:36:41 +0100 |
wenzelm |
ProofContext.read_class/read_type_name_proper;
|
changeset |
files
|
| Tue, 09 Mar 2010 14:35:02 +0100 |
wenzelm |
added ProofContext.tsig_of -- proforma version for local name space only, not logical content;
|
changeset |
files
|
| Tue, 09 Mar 2010 14:29:47 +0100 |
wenzelm |
simplified Syntax.basic_syntax (again);
|
changeset |
files
|
| Tue, 09 Mar 2010 14:55:25 +0100 |
wenzelm |
tuned -- eliminated Sign.intern_sort;
|
changeset |
files
|
| Tue, 09 Mar 2010 14:18:06 +0100 |
wenzelm |
renamed mk_const_def to legacy_const_def, because of slightly odd Sign.intern_term;
|
changeset |
files
|
| Tue, 09 Mar 2010 09:25:23 +0100 |
blanchet |
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
|
changeset |
files
|
| Mon, 08 Mar 2010 15:20:40 -0800 |
huffman |
merged
|
changeset |
files
|
| Mon, 08 Mar 2010 14:42:40 -0800 |
huffman |
remove unnecessary error handling code
|
changeset |
files
|
| Mon, 08 Mar 2010 14:12:51 -0800 |
huffman |
construct fully typed goal in proof of induction rule
|
changeset |
files
|
| 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
|
changeset |
files
|
| Mon, 08 Mar 2010 12:43:44 -0800 |
huffman |
remove redundant function arguments
|
changeset |
files
|
| Mon, 08 Mar 2010 12:36:26 -0800 |
huffman |
include take_info within take_induct_info type
|
changeset |
files
|
| Mon, 08 Mar 2010 12:21:07 -0800 |
huffman |
pass take_info as an argument to comp_theorems
|
changeset |
files
|
| Mon, 08 Mar 2010 11:58:40 -0800 |
huffman |
pass take_induct_info as an argument to comp_theorems
|
changeset |
files
|
| Mon, 08 Mar 2010 11:48:29 -0800 |
huffman |
add type take_induct_info
|
changeset |
files
|
| Mon, 08 Mar 2010 11:34:53 -0800 |
huffman |
generate take_induct lemmas
|
changeset |
files
|
| Mon, 08 Mar 2010 09:37:03 -0800 |
huffman |
move proofs of reach and take lemmas to domain_take_proofs.ML
|
changeset |
files
|
| Mon, 08 Mar 2010 09:33:05 -0800 |
huffman |
move lemmas from Domain.thy to Domain_Aux.thy
|
changeset |
files
|
| Mon, 08 Mar 2010 08:12:48 -0800 |
huffman |
move take-proofs stuff into new theory Domain_Aux.thy
|
changeset |
files
|
| Mon, 08 Mar 2010 07:37:11 -0800 |
huffman |
add type take_info
|
changeset |
files
|
| Mon, 08 Mar 2010 07:22:30 -0800 |
huffman |
add function add_qualified_def
|
changeset |
files
|
| Mon, 08 Mar 2010 17:37:09 +0100 |
haftmann |
merged
|
changeset |
files
|
| Mon, 08 Mar 2010 14:41:56 +0100 |
haftmann |
proper ML interface; further polishing
|
changeset |
files
|
| Mon, 08 Mar 2010 13:22:41 +0100 |
haftmann |
code simplification and tuning
|
changeset |
files
|
| Mon, 08 Mar 2010 15:00:34 +0100 |
berghofe |
Added inducts field to inductive_result.
|
changeset |
files
|
| Mon, 08 Mar 2010 09:38:59 +0100 |
haftmann |
transfer: avoid camel case, more standard coding conventions, misc tuning
|
changeset |
files
|