| Mon, 17 Feb 2014 18:18:27 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 13:31:42 +0100 |
blanchet |
tuning: moved code where it belongs
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 13:45:29 +0100 |
traytel |
register bnfs for (co)datatypes under their proper name (lost in af71b753c459)
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
adapted theories to 'xxx_case' to 'case_xxx'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed 'nat_{case,rec}' to '{case,rec}_nat'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
adapted theories to '{case,rec}_{list,option}' names
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 12:16:59 +0100 |
traytel |
use Local_Theory.define instead of Specification.definition for internal constants
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 10:02:36 +0100 |
traytel |
less hermetic tactics
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
tuned names
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
made BNF compile after move to HOL
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
adjusted comments
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
avoid nested 'Tools' directories
|
file |
diff |
annotate
| base
|