| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 16:25:47 +0200 |
wenzelm |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
file |
diff |
annotate
|
| Sat, 23 Apr 2011 13:00:19 +0200 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| Fri, 22 Oct 2010 18:38:59 +0200 |
bulwahn |
splitting Hotel Key card example into specification and the two tests for counter example generation
|
file |
diff |
annotate
|
| Thu, 30 Sep 2010 10:48:12 +0200 |
bulwahn |
finding the counterexample with different options (manually limited precisely, manually limited global, automatically limited global)
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 13:49:08 +0200 |
bulwahn |
adapting examples
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 12:04:34 +0200 |
nipkow |
merged
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 11:51:53 +0200 |
bulwahn |
adapting example files
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 15:21:56 +0200 |
bulwahn |
adapting and tuning example theories
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 08:00:56 +0200 |
bulwahn |
changing order of premises generated when flattening functions in premises; adapting example for second attack for hotel key card system
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 08:00:55 +0200 |
bulwahn |
added further hotel key card attack in example file
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 08:00:53 +0200 |
bulwahn |
storing options for prolog code generation in the theory
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 08:00:52 +0200 |
bulwahn |
adapting example files to latest changes
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 16:59:53 +0200 |
bulwahn |
changing hotel trace definition; adding simple handling of numerals on natural numbers
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 16:59:51 +0200 |
bulwahn |
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 16:59:50 +0200 |
bulwahn |
invocation of values for prolog execution does not require invocation of code_pred anymore
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 16:59:49 +0200 |
bulwahn |
adding hotel keycard example for prolog generation
|
file |
diff |
annotate
|