| Sun, 06 Mar 2016 20:39:19 +0100 |
traytel |
less resetting of local theories
|
file |
diff |
annotate
|
| Sat, 05 Mar 2016 12:49:47 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 17:08:36 +0100 |
blanchet |
making 'pred_inject' a first-class BNF citizen
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 17:08:03 +0100 |
blanchet |
refactoring
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 15:18:06 +0100 |
traytel |
derive transfer rule for predicator
|
file |
diff |
annotate
|
| Tue, 16 Feb 2016 22:28:19 +0100 |
traytel |
make predicator a first-class bnf citizen
|
file |
diff |
annotate
|
| Tue, 01 Dec 2015 22:21:37 +0100 |
blanchet |
reverted inadvertently qfinished/pushed change r164eeb2ab675
|
file |
diff |
annotate
|
| Tue, 01 Dec 2015 13:07:41 +0100 |
blanchet |
set "transfer_rule" attribute more generously
|
file |
diff |
annotate
|
| Wed, 07 Oct 2015 10:02:43 +0200 |
blanchet |
disable generation of 'case_transfer' for 'nibble', due to quadratic proof -- to make 'HOL-Proofs' happier
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 17:44:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 16 Jul 2015 12:23:22 +0200 |
traytel |
{r,e,d,f}tac with proper context in BNF
|
file |
diff |
annotate
|
| Tue, 18 Nov 2014 16:19:57 +0100 |
kuncar |
tuned; store pred_simps
|
file |
diff |
annotate
|
| Tue, 18 Nov 2014 16:19:51 +0100 |
kuncar |
added pred_def, rel_eq_onp tuned
|
file |
diff |
annotate
|
| Tue, 28 Apr 2015 13:30:28 +0200 |
blanchet |
allow sorts on dead variables in BNFs
|
file |
diff |
annotate
|
| Fri, 27 Mar 2015 11:20:46 +0100 |
blanchet |
more graceful failure if some of the involved BNFs have no data
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2015 19:08:04 +0100 |
traytel |
eliminated some clones of Proof_Context.cterm_of
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Mon, 05 Jan 2015 06:56:15 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 10 Nov 2014 21:49:48 +0100 |
wenzelm |
proper context for assume_tac (atac remains as fall-back without context);
|
file |
diff |
annotate
|
| Sat, 25 Oct 2014 11:53:35 +0200 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
| Mon, 20 Oct 2014 17:56:23 +0200 |
kuncar |
register transfer rules from BNF and FP_Sugar
|
file |
diff |
annotate
|
| Mon, 20 Oct 2014 17:56:21 +0200 |
kuncar |
refactored
|
file |
diff |
annotate
|
| Mon, 13 Oct 2014 18:45:48 +0200 |
wenzelm |
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
|
file |
diff |
annotate
|
| Fri, 26 Sep 2014 14:41:08 +0200 |
desharna |
refactor fp_sugar move theorems
|
file |
diff |
annotate
|
| Wed, 17 Sep 2014 11:12:46 +0200 |
blanchet |
added missing 'restore' in 'transfer' plugin
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 19:21:07 +0200 |
blanchet |
honour sorts in N2M
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 16:09:10 +0200 |
blanchet |
made code work also in the presence of deads
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 15:11:37 +0200 |
blanchet |
use right sort constraints
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
pretend code generation is a ctr_sugar plugin
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
named interpretations
|
file |
diff |
annotate
|
| Thu, 04 Sep 2014 09:02:43 +0200 |
blanchet |
tuned size function generation
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 22:49:05 +0200 |
blanchet |
introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales
|
file |
diff |
annotate
|
| Mon, 11 Aug 2014 10:43:03 +0200 |
traytel |
use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed)
|
file |
diff |
annotate
|
| Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 17:57:56 +0200 |
kuncar |
predicator simplification rules: support also partially specialized types e.g. 'a * nat
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
localize new size function generation code
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
manual merge + added 'rel_distincts' field to record for symmetry
|
file |
diff |
annotate
|
| Fri, 11 Apr 2014 16:59:42 +0200 |
kuncar |
observe also DEADID BNFs and associate the conjunction in rel_inject to the right
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:18 +0200 |
kuncar |
setup for Transfer and Lifting from BNF; tuned thm names
|
file |
diff |
annotate
|