| Thu, 10 Apr 2014 17:48:15 +0200 |
kuncar |
abstract Domainp in relator_domain rules => more natural statement of the rule
|
file |
diff |
annotate
|
| Sat, 22 Mar 2014 18:19:57 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:40:33 +0100 |
blanchet |
renamed 'fun_rel' to 'rel_fun'
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 15:02:19 +0100 |
kuncar |
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 23:03:47 +0100 |
kuncar |
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
|
file |
diff |
annotate
|
| Tue, 31 Dec 2013 14:29:16 +0100 |
wenzelm |
proper context for norm_hhf and derived operations;
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| Mon, 16 Sep 2013 11:54:57 +0200 |
kuncar |
public access to the raw transfer rules - for restoring transferring
|
file |
diff |
annotate
|
| Thu, 22 Aug 2013 17:19:51 +0200 |
kuncar |
delete corresponding compound lhs and rhs when a transfer rule is deleted; tuned
|
file |
diff |
annotate
|
| Thu, 22 Aug 2013 17:19:44 +0200 |
kuncar |
publish a private function
|
file |
diff |
annotate
|
| Wed, 21 Aug 2013 16:51:50 +0200 |
kuncar |
double check that lhs or rhs really matches a subterm in a goal when creating a hole in a skeleton (Net.net does only rough matching)
|
file |
diff |
annotate
|
| Fri, 16 Aug 2013 21:28:05 +0200 |
wenzelm |
standardized aliases;
|
file |
diff |
annotate
|
| Wed, 07 Aug 2013 15:40:59 +0200 |
kuncar |
contract equalities in transfer and transfer domain rules when they are registered
|
file |
diff |
annotate
|
| Wed, 07 Aug 2013 15:40:29 +0200 |
kuncar |
expand equalities in the transfer relation in transfer_prover if the relation doesn't follow the functional structure
|
file |
diff |
annotate
|
| Mon, 10 Jun 2013 06:08:12 -0700 |
huffman |
implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
|
file |
diff |
annotate
|
| Sat, 08 Jun 2013 19:40:19 -0700 |
huffman |
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
|
file |
diff |
annotate
|
| Wed, 15 May 2013 12:13:38 +0200 |
kuncar |
abstract equalities only in a correspondence relation in a transfer domain rule
|
file |
diff |
annotate
|
| Mon, 13 May 2013 13:59:04 +0200 |
kuncar |
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
|
file |
diff |
annotate
|
| Mon, 13 May 2013 12:13:24 +0200 |
kuncar |
try to detect assumptions of transfer rules that are in a shape of a transfer rule
|
file |
diff |
annotate
|
| Mon, 13 May 2013 12:13:24 +0200 |
kuncar |
publish a private function
|
file |
diff |
annotate
|
| Sat, 16 Mar 2013 20:51:23 +0100 |
kuncar |
fixing transfer tactic - unfold fully identity relation by using relator_eq
|
file |
diff |
annotate
|
| Fri, 08 Mar 2013 13:14:23 +0100 |
kuncar |
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
|
file |
diff |
annotate
|
| Thu, 28 Feb 2013 16:54:52 +0100 |
wenzelm |
just one HOLogic.Trueprop_conv, with regular exception CTERM;
|
file |
diff |
annotate
|
| Wed, 24 Oct 2012 18:43:25 +0200 |
huffman |
transfer package: error message if preprocessing goal to object-logic formula fails
|
file |
diff |
annotate
|
| Wed, 24 Oct 2012 18:43:25 +0200 |
huffman |
transfer package: add test to prevent trying to make cterms from open terms
|
file |
diff |
annotate
|
| Wed, 24 Oct 2012 18:43:25 +0200 |
huffman |
transfer package: more flexible handling of equality relations using is_equality predicate
|
file |
diff |
annotate
|
| Thu, 27 Sep 2012 20:30:30 +0200 |
kuncar |
new get function for non-symmetric relator_eq & tuned
|
file |
diff |
annotate
|
| Sat, 02 Jun 2012 08:27:29 +0200 |
huffman |
transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
|
file |
diff |
annotate
|
| Fri, 01 Jun 2012 11:55:06 +0200 |
huffman |
transfer method now avoids generalizing over free variables that are known to appear in registered transfer rules
|
file |
diff |
annotate
|
| Fri, 01 Jun 2012 11:54:34 +0200 |
huffman |
unify theory-data structures for transfer package
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 17:14:13 +0200 |
huffman |
allow transfer tactic to leave extra unsolved subgoals if transfer rules are missing
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 14:07:31 +0200 |
huffman |
implement transfer tactic with more scalable forward proof methods
|
file |
diff |
annotate
|
| Sat, 21 Apr 2012 20:52:33 +0200 |
huffman |
enable variant of transfer method that proves an implication instead of an equivalence
|
file |
diff |
annotate
|
| Fri, 20 Apr 2012 22:49:40 +0200 |
huffman |
rename 'correspondence' method to 'transfer_prover'
|
file |
diff |
annotate
|
| Fri, 20 Apr 2012 10:18:08 +0200 |
huffman |
make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 11:52:07 +0200 |
huffman |
use simpler method for preserving bound variable names in transfer tactic
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 17:44:39 +0200 |
huffman |
add option to transfer method for specifying variables not to generalize over
|
file |
diff |
annotate
|
| Tue, 17 Apr 2012 14:00:09 +0200 |
huffman |
make transfer method more deterministic by using SOLVED' on some subgoals
|
file |
diff |
annotate
|
| Tue, 17 Apr 2012 11:03:08 +0200 |
huffman |
add theory data for relator identity rules;
|
file |
diff |
annotate
|
| Wed, 04 Apr 2012 16:05:52 +0200 |
huffman |
transfer method generalizes over free variables in goal
|
file |
diff |
annotate
|
| Wed, 04 Apr 2012 16:03:01 +0200 |
huffman |
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
|
file |
diff |
annotate
|
| Wed, 04 Apr 2012 07:47:42 +0200 |
huffman |
add type annotations to make SML happy (cf. ec6187036495)
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 22:31:00 +0200 |
huffman |
new transfer proof method
|
file |
diff |
annotate
|
| Wed, 15 Feb 2012 23:19:30 +0100 |
wenzelm |
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
|
file |
diff |
annotate
|
| Wed, 23 Nov 2011 22:59:39 +0100 |
wenzelm |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file |
diff |
annotate
|
| Wed, 09 Nov 2011 21:36:18 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Thu, 08 Jul 2010 16:19:24 +0200 |
haftmann |
tuned titles
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 13:56:33 +0100 |
haftmann |
meaningful transfer certificate
|
file |
diff |
annotate
|
| Thu, 11 Mar 2010 09:09:43 +0100 |
haftmann |
made smlnj happy
|
file |
diff |
annotate
|
| Tue, 09 Mar 2010 21:19:49 +0100 |
haftmann |
clarified transfer code proper; more natural declaration of return rules
|
file |
diff |
annotate
|
| Tue, 09 Mar 2010 18:31:37 +0100 |
haftmann |
data administration using canonical functorial operations
|
file |
diff |
annotate
|
| Tue, 09 Mar 2010 16:15:19 +0100 |
haftmann |
tuned data structures; using AList.map_default
|
file |
diff |
annotate
|
| Tue, 09 Mar 2010 15:47:16 +0100 |
haftmann |
consistent field names; tuned interface
|
file |
diff |
annotate
|
| Mon, 08 Mar 2010 14:41:56 +0100 |
haftmann |
proper ML interface; further polishing
|
file |
diff |
annotate
|
| Mon, 08 Mar 2010 13:22:41 +0100 |
haftmann |
code simplification and tuning
|
file |
diff |
annotate
|
| Mon, 08 Mar 2010 09:38:59 +0100 |
haftmann |
transfer: avoid camel case, more standard coding conventions, misc tuning
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 08:46:12 +0100 |
haftmann |
dropped dead code; adhere more closely to standard coding conventions
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 11:41:39 +0100 |
haftmann |
join entries properly on theory merge
|
file |
diff |
annotate
|