| Mon, 08 Sep 2014 23:09:25 +0200 |
blanchet |
made 'lifting' plugin more robust
|
changeset |
files
|
| Mon, 08 Sep 2014 23:09:24 +0200 |
blanchet |
tuned command descriptions
|
changeset |
files
|
| Mon, 08 Sep 2014 23:09:23 +0200 |
blanchet |
generate better internal names, with name of the target type in it
|
changeset |
files
|
| Mon, 08 Sep 2014 23:09:04 +0200 |
blanchet |
removed comment (yes, this is different -- add_typedef_global will fail in a locale with assumptions)
|
changeset |
files
|
| Mon, 08 Sep 2014 23:04:18 +0200 |
blanchet |
added flag to 'typedef' to allow concealed definitions
|
changeset |
files
|
| Mon, 08 Sep 2014 23:04:18 +0200 |
blanchet |
ported old Nominal to use new datatypes
|
changeset |
files
|
| Mon, 08 Sep 2014 20:42:52 +0200 |
traytel |
made tactic even more robust w.r.t. dead variables
|
changeset |
files
|
| Mon, 08 Sep 2014 19:21:19 +0200 |
blanchet |
made N2M work with sort constraints (cf. TODO)
|
changeset |
files
|
| Mon, 08 Sep 2014 19:21:14 +0200 |
blanchet |
compile
|
changeset |
files
|
| Mon, 08 Sep 2014 19:21:07 +0200 |
blanchet |
honour sorts in N2M
|
changeset |
files
|
| Mon, 08 Sep 2014 16:51:35 +0200 |
blanchet |
proper sort constraints in map and rel theorems
|
changeset |
files
|
| Mon, 08 Sep 2014 16:22:26 +0200 |
blanchet |
made new countable tactic work with sorts other than 'type'
|
changeset |
files
|
| Mon, 08 Sep 2014 16:14:21 +0200 |
blanchet |
adapted examples to latest changes
|
changeset |
files
|
| Mon, 08 Sep 2014 16:09:10 +0200 |
blanchet |
made code work also in the presence of deads
|
changeset |
files
|
| Mon, 08 Sep 2014 15:54:33 +0200 |
blanchet |
export right sorts
|
changeset |
files
|
| Mon, 08 Sep 2014 15:12:35 +0200 |
blanchet |
test sorts
|
changeset |
files
|
| Mon, 08 Sep 2014 15:11:37 +0200 |
blanchet |
use right sort constraints
|
changeset |
files
|
| Mon, 08 Sep 2014 14:04:03 +0200 |
blanchet |
never include hidden names -- these cannot be referenced afterward
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:57 +0200 |
blanchet |
use compatibility layer
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:46 +0200 |
blanchet |
made SML/NJ happire
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:40 +0200 |
blanchet |
export useful functions for users of (co)recursors
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:35 +0200 |
blanchet |
improved caching
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:13 +0200 |
blanchet |
compile
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:08 +0200 |
blanchet |
wildcards in plugins
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:02 +0200 |
blanchet |
improved 'datatype_compat' further for recursion through functions
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:02 +0200 |
blanchet |
no type-based lookup -- these fail in the general, ambiguous case
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:02 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:02 +0200 |
blanchet |
more examples/tests
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:02 +0200 |
blanchet |
tuned docs
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
properly note theorems for split recursors
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
updated docs
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
export one more ML function
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
more compatibility documentation
|
changeset |
files
|
| Mon, 08 Sep 2014 13:56:28 +0200 |
blanchet |
refactored MaSh files to avoid regenerating exports on each eval
|
changeset |
files
|
| Mon, 08 Sep 2014 13:56:27 +0200 |
blanchet |
added missing 'transpose'
|
changeset |
files
|
| Mon, 08 Sep 2014 13:56:27 +0200 |
blanchet |
the kind is now always the empty string -- can no longer distinguish between user theorems and package theorems in a semi-reliable way
|
changeset |
files
|
| Mon, 08 Sep 2014 09:52:06 +0200 |
traytel |
made tactic more robust w.r.t. dead variables
|
changeset |
files
|
| Sun, 07 Sep 2014 17:51:32 +0200 |
haftmann |
restrictive options for class dependencies
|
changeset |
files
|
| Sun, 07 Sep 2014 17:51:28 +0200 |
haftmann |
separated class_deps command into separate file
|
changeset |
files
|
| Sun, 07 Sep 2014 14:39:23 +0200 |
steckerm |
Added translation for lambda expressions in terms.
|
changeset |
files
|
| Sun, 07 Sep 2014 09:49:05 +0200 |
haftmann |
explicit theory with additional, less commonly used list operations
|
changeset |
files
|
| Sun, 07 Sep 2014 09:49:01 +0200 |
haftmann |
generalized
|
changeset |
files
|
| Sat, 06 Sep 2014 20:12:36 +0200 |
haftmann |
theory about sum and product on function bodies
|
changeset |
files
|
| Sat, 06 Sep 2014 20:12:34 +0200 |
haftmann |
theory about lexicographic ordering on functions
|
changeset |
files
|
| Sat, 06 Sep 2014 20:12:32 +0200 |
haftmann |
added various facts
|
changeset |
files
|
| Fri, 05 Sep 2014 16:09:03 +0100 |
paulson |
Generalised card_length_listsum to all m
|
changeset |
files
|
| Fri, 05 Sep 2014 14:58:13 +0200 |
nipkow |
added lemma
|
changeset |
files
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
updated docs
|
changeset |
files
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
pretend code generation is a ctr_sugar plugin
|
changeset |
files
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
updated docs
|
changeset |
files
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
added 'plugins' option to control which hooks are enabled
|
changeset |
files
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
introduced mechanism to filter interpretations
|
changeset |
files
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
fixed infinite loops in 'register' functions + more uniform API
|
changeset |
files
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
named interpretations
|
changeset |
files
|
| Fri, 05 Sep 2014 00:41:00 +0200 |
blanchet |
centralized and cleaned up naming handling
|
changeset |
files
|
| Thu, 04 Sep 2014 14:02:37 +0200 |
hoelzl |
cleanup Wfrec; introduce dependent_wf/wellorder_choice
|
changeset |
files
|
| Thu, 04 Sep 2014 11:53:39 +0200 |
blanchet |
tuned Nitpick and Refute examples, which are too slow on some testing machines
|
changeset |
files
|
| Thu, 04 Sep 2014 11:20:59 +0200 |
blanchet |
tweaked setup for datatype realizer
|
changeset |
files
|
| Thu, 04 Sep 2014 09:02:43 +0200 |
blanchet |
renamed internal constant
|
changeset |
files
|
| Thu, 04 Sep 2014 09:02:43 +0200 |
blanchet |
moved code around
|
changeset |
files
|
| Thu, 04 Sep 2014 09:02:43 +0200 |
blanchet |
tuned size function generation
|
changeset |
files
|
| Thu, 04 Sep 2014 09:02:36 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 03 Sep 2014 22:49:05 +0200 |
blanchet |
introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:48 +0200 |
blanchet |
tuned ctr_sugar database handling
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:35 +0200 |
blanchet |
tuned BNF database handling
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:09 +0200 |
blanchet |
intelligible errors instead of tactic failures
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
reenabled yet another example
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
made new tactic even more robust
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
reenabled more examples
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
fixed tactic for n-way mutual recursion, n >= 4 (balanced conjunctions confuse the tactic)
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
reintroduced more examples
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
improved tactic further
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
reenabled example
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
improved new countability tactic
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
'prove_sorry' is too dangerous here -- the tactic is sometimes applied to non-theorems
|
changeset |
files
|
| Wed, 03 Sep 2014 22:47:05 +0200 |
blanchet |
more robust exception handling
|
changeset |
files
|
| Wed, 03 Sep 2014 22:46:54 +0200 |
blanchet |
added tests for new 'countable_datatype' proof method
|
changeset |
files
|
| Wed, 03 Sep 2014 12:30:25 +0200 |
traytel |
lessen the burden on the caller: sort where necessary in n2m
|
changeset |
files
|
| Wed, 03 Sep 2014 09:43:00 +0200 |
blanchet |
added compatibility function
|
changeset |
files
|
| Wed, 03 Sep 2014 00:31:38 +0200 |
blanchet |
added countable tactic for new-style datatypes
|
changeset |
files
|
| Wed, 03 Sep 2014 00:31:37 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:32 +0200 |
blanchet |
registered 'typerep' as countable again
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:30 +0200 |
blanchet |
moved old datatype material around
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:28 +0200 |
blanchet |
removed vacuous theorem references
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:27 +0200 |
blanchet |
commented out failing tactic (now that 'typerep' is defined using the new package
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:26 +0200 |
blanchet |
tuned imports
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:25 +0200 |
blanchet |
use 'datatype_new'
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:24 +0200 |
blanchet |
use 'datatype_new' in 'Main'
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:23 +0200 |
blanchet |
take out 'x = C' of the simplifier for unit types
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:22 +0200 |
blanchet |
giving up calling 'datatype_compat' in a locale -- causes trouble with extensions
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:22 +0200 |
blanchet |
ported 'Statespace' to support new datatypes as well
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:21 +0200 |
blanchet |
use 'datatype_new' in Quickcheck examples
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:19 +0200 |
blanchet |
more compatibility functions
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:18 +0200 |
blanchet |
codatatypes are not datatypes
|
changeset |
files
|
| Wed, 03 Sep 2014 00:06:17 +0200 |
blanchet |
ported Quickcheck to support new datatypes better
|
changeset |
files
|
| Tue, 02 Sep 2014 23:59:49 +0200 |
blanchet |
removed more slow Refute tests
|
changeset |
files
|
| Tue, 02 Sep 2014 23:59:46 +0200 |
blanchet |
tuned Refute example
|
changeset |
files
|
| Tue, 02 Sep 2014 16:38:26 +0200 |
steckerm |
Some work on the new waldmeister integration
|
changeset |
files
|
| Tue, 02 Sep 2014 14:40:32 +0200 |
boehmes |
merged
|
changeset |
files
|
| Tue, 02 Sep 2014 14:40:14 +0200 |
boehmes |
replay Z3 rewrite steps that lift if-then-else expressions
|
changeset |
files
|
| Tue, 02 Sep 2014 13:40:03 +0200 |
traytel |
test discriminators/selectors in BNF regression suite
|
changeset |
files
|
| Tue, 02 Sep 2014 12:13:32 +0200 |
blanchet |
merge
|
changeset |
files
|
| Tue, 02 Sep 2014 12:11:04 +0200 |
blanchet |
made SML/NJ happier
|
changeset |
files
|
| Tue, 02 Sep 2014 12:09:13 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 02 Sep 2014 09:28:23 +0200 |
traytel |
silenced nonexhaustive primrec warnings
|
changeset |
files
|
| Tue, 02 Sep 2014 08:24:42 +0200 |
haftmann |
more convenient printing of real numbers after evaluation
|
changeset |
files
|
| Mon, 01 Sep 2014 19:58:25 +0200 |
blanchet |
avoid more 'bad background theory' issues
|
changeset |
files
|
| Mon, 01 Sep 2014 19:57:48 +0200 |
blanchet |
ported TFL to mixture of old and new datatypes
|
changeset |
files
|
| Mon, 01 Sep 2014 19:28:00 +0200 |
blanchet |
drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
|
changeset |
files
|
| Mon, 01 Sep 2014 18:42:02 +0200 |
blanchet |
ported to use new-style datatypes
|
changeset |
files
|
| Mon, 01 Sep 2014 17:34:03 +0200 |
blanchet |
ported Refute to use new datatypes when possible
|
changeset |
files
|
| Mon, 01 Sep 2014 16:34:40 +0200 |
blanchet |
renamed BNF theories
|
changeset |
files
|
| Mon, 01 Sep 2014 16:34:39 +0200 |
blanchet |
renamed '(BNF_)Constructions_on_Wellorders' to '(BNF_)Wellorder_Constructions'
|
changeset |
files
|
| Mon, 01 Sep 2014 16:34:38 +0200 |
blanchet |
added primrec compatibility function
|
changeset |
files
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
more work on compatibility interfaces
|
changeset |
files
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
added compatibility examples/tests
|
changeset |
files
|