| Fri, 05 Sep 2014 00:41:00 +0200 |
blanchet |
centralized and cleaned up naming handling
|
file |
diff |
annotate
|
| Thu, 04 Sep 2014 11:20:59 +0200 |
blanchet |
tweaked setup for datatype realizer
|
file |
diff |
annotate
|
| Thu, 04 Sep 2014 09:02:43 +0200 |
blanchet |
moved code around
|
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
|
| Wed, 03 Sep 2014 22:47:35 +0200 |
blanchet |
tuned BNF database handling
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 00:31:37 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
more compatibility between old- and new-style datatypes
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
added theory-based getters for convenience
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
made transfer functions slightly more general
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 13:23:39 +0200 |
desharna |
generate 'rel_transfer' for BNFs
|
file |
diff |
annotate
|
| Fri, 29 Aug 2014 14:36:51 +0200 |
desharna |
generate 'disc_transfer' for (co)datatypes
|
file |
diff |
annotate
|
| Fri, 29 Aug 2014 14:21:24 +0200 |
desharna |
generate 'case_transfer' for (co)datatypes
|
file |
diff |
annotate
|
| Wed, 27 Aug 2014 13:05:59 +0200 |
blanchet |
removed not so interesting 'set_empty'
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 23:17:51 +0200 |
wenzelm |
tuned signature -- moved type src to Token, without aliases;
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 16:46:31 +0200 |
desharna |
generate 'ctr_transfer' for (co)datatypes
|
file |
diff |
annotate
|
| Mon, 18 Aug 2014 19:16:30 +0200 |
blanchet |
set attributes on 'set_cases' theorem
|
file |
diff |
annotate
|
| Mon, 18 Aug 2014 17:19:58 +0200 |
blanchet |
reordered some (co)datatype property names for more consistency
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 13:20:54 +0200 |
desharna |
generate 'rel_map' theorem for BNFs
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 17:18:12 +0200 |
blanchet |
avoid needless (and wrong w.r.t. sorts) generation of type variables; tuned whitespaces;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 12:31:42 +0200 |
desharna |
generate 'set_cases' theorem for (co)datatypes
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 12:01:37 +0200 |
desharna |
generate 'set_intros' theorem for (co)datatypes
|
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
|
| Sun, 10 Aug 2014 14:34:43 +0200 |
wenzelm |
merged -- with manual conflict resolution for src/HOL/SMT_Examples/SMT_Examples.certs2, src/HOL/SMT_Examples/SMT_Word_Examples.certs2, src/Doc/Prog_Prove/document/intro-isabelle.tex;
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 09:40:28 +0200 |
blanchet |
correctly resolve selector names in default value equations
|
file |
diff |
annotate
|
| Mon, 28 Jul 2014 12:31:30 +0200 |
desharna |
made tactic more robust w.r.t. dead variables; tuned;
|
file |
diff |
annotate
|
| Thu, 07 Aug 2014 12:17:41 +0200 |
blanchet |
generate nicer 'set' theorems for (co)datatypes
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 10:50:28 +0200 |
desharna |
generate 'set_induct' theorem for codatatypes
|
file |
diff |
annotate
|
| Fri, 25 Jul 2014 11:26:10 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 23:01:23 +0200 |
blanchet |
tuned code
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 00:24:00 +0200 |
blanchet |
repaired named derivations
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 00:24:00 +0200 |
blanchet |
use the noted theorem whenever possible, also in 'BNF_Def'
|
file |
diff |
annotate
|
| Thu, 17 Jul 2014 10:29:09 +0200 |
desharna |
fix bug caused by bad context
|
file |
diff |
annotate
|
| Thu, 17 Jul 2014 10:28:32 +0200 |
desharna |
add mk_Trueprop_mem utility function
|
file |
diff |
annotate
|
| Wed, 16 Jul 2014 10:22:06 +0200 |
desharna |
refactor commonly used functions
|
file |
diff |
annotate
|
| Wed, 16 Jul 2014 10:13:00 +0200 |
desharna |
generate 'rel_sel' theorem for (co)datatypes
|
file |
diff |
annotate
|
| Wed, 16 Jul 2014 10:11:25 +0200 |
desharna |
fix rel_cases
|
file |
diff |
annotate
|
| Tue, 15 Jul 2014 00:35:07 +0200 |
blanchet |
took out 'rel_cases' for now because of failing tactic
|
file |
diff |
annotate
|
| Wed, 09 Jul 2014 11:54:01 +0200 |
blanchet |
made SML/NJ happier
|
file |
diff |
annotate
|
| Mon, 07 Jul 2014 16:06:46 +0200 |
desharna |
generate 'rel_cases' theorem for (co)datatypes
|
file |
diff |
annotate
|
| Thu, 03 Jul 2014 11:30:02 +0200 |
desharna |
generate 'rel_intros' theorem for (co)datatypes
|
file |
diff |
annotate
|
| Wed, 02 Jul 2014 17:01:49 +0200 |
desharna |
generate 'corec_code' theorem for codatatypes
|
file |
diff |
annotate
|
| Tue, 01 Jul 2014 17:01:28 +0200 |
desharna |
generate 'rel_induct' theorem for datatypes
|
file |
diff |
annotate
|
| Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
| Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
tuned variable names
|
file |
diff |
annotate
|
| Tue, 24 Jun 2014 13:48:14 +0200 |
desharna |
tune the implementation of 'rel_coinduct'
|
file |
diff |
annotate
|
| Tue, 24 Jun 2014 13:48:14 +0200 |
desharna |
generate 'rel_coinduct' theorem for codatatypes
|
file |
diff |
annotate
|
| Tue, 24 Jun 2014 13:48:14 +0200 |
desharna |
generate 'rel_coinduct0' theorem for codatatypes
|
file |
diff |
annotate
|
| Wed, 18 Jun 2014 17:42:24 +0200 |
blanchet |
made tactic more robust in the face of 'primcorec' specifications containing 'case_sum'
|
file |
diff |
annotate
|
| Mon, 16 Jun 2014 19:18:10 +0200 |
blanchet |
fixed postprocessing of 'coinduct' formula to obtain right property format (without needless hypotheses)
|
file |
diff |
annotate
|
| Tue, 10 Jun 2014 21:15:57 +0200 |
blanchet |
changed syntax of map: and rel: arguments to BNF-based datatypes
|
file |
diff |
annotate
|
| Tue, 10 Jun 2014 19:51:00 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 10 Jun 2014 12:16:22 +0200 |
blanchet |
use 'where' clause for selector default value syntax
|
file |
diff |
annotate
|
| Tue, 10 Jun 2014 11:38:53 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 02 Jun 2014 14:29:20 +0200 |
desharna |
generate 'sel_set' theorem for (co)datatypes
|
file |
diff |
annotate
|
| Tue, 27 May 2014 17:32:42 +0200 |
blanchet |
don't generate discriminators and selectors for 'datatype_new' unless the user asked for it
|
file |
diff |
annotate
|
| Mon, 26 May 2014 16:32:55 +0200 |
blanchet |
got rid of '=:' squiggly
|
file |
diff |
annotate
|
| Wed, 21 May 2014 18:55:34 +0200 |
desharna |
generate 'sel_map[simp]' theorem for (co)datatypes and tuning 'disc_map_iff'
|
file |
diff |
annotate
|
| Thu, 15 May 2014 16:15:44 +0200 |
desharna |
generate 'disc_map_iff[simp]' theorem for (co)datatypes
|
file |
diff |
annotate
|