| Thu, 16 Sep 2010 15:37:12 +0200 |
wenzelm |
Isar "default" step needs to fail for solved problems, for clear distinction of '.' and '..' for example -- amending lapse introduced in 9de4d64eee3b (April 2004);
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 16:44:20 +0200 |
bulwahn |
adding two more examples to example theory
|
file |
diff |
annotate
|
| Fri, 10 Sep 2010 10:59:10 +0200 |
bulwahn |
adding another String.literal example
|
file |
diff |
annotate
|
| Thu, 09 Sep 2010 17:23:08 +0200 |
bulwahn |
adding an example with integers and String.literals
|
file |
diff |
annotate
|
| Thu, 09 Sep 2010 17:23:07 +0200 |
bulwahn |
adding an example to show how code_pred must be invoked with locales
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 11:51:53 +0200 |
bulwahn |
renewing specification in example file; adding invocation in example file
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 16:47:55 +0200 |
bulwahn |
added support for xsymbol syntax for mode annotations in code_pred command
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 16:45:51 +0200 |
bulwahn |
added an example with a free function variable to the Predicate Compile examples
|
file |
diff |
annotate
|
| Wed, 21 Apr 2010 12:10:52 +0200 |
bulwahn |
added examples for detecting switches
|
file |
diff |
annotate
|
| Wed, 21 Apr 2010 12:10:52 +0200 |
bulwahn |
adopting examples to changes in the predicate compiler
|
file |
diff |
annotate
|
| Wed, 21 Apr 2010 12:10:52 +0200 |
bulwahn |
added further inlining of boolean constants to the predicate compiler
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 21:28:09 +0200 |
wenzelm |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
file |
diff |
annotate
|
| Wed, 31 Mar 2010 16:44:41 +0200 |
bulwahn |
adding examples of function predicate replacement and arithmetic examples for the predicate compiler; tuned
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 17:30:56 +0200 |
bulwahn |
adding skip_proof in the examples because proof procedure cannot handle alternative compilations yet
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 17:40:44 +0100 |
bulwahn |
adopting examples to Library move
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 17:40:43 +0100 |
bulwahn |
moved examples for the predicate compiler into its own session Predicate_Compile_Examples to slenderise the HOL-ex session
|
file |
diff |
annotate
|