src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2011-04-23 wenzelm 2011-04-23 modernized specifications;
2010-10-22 bulwahn 2010-10-22 splitting Hotel Key card example into specification and the two tests for counter example generation
2010-09-30 bulwahn 2010-09-30 finding the counterexample with different options (manually limited precisely, manually limited global, automatically limited global)
2010-09-16 bulwahn 2010-09-16 adapting examples
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 merged
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-09-07 bulwahn 2010-09-07 adapting example files
2010-08-31 bulwahn 2010-08-31 adapting and tuning example theories
2010-08-31 bulwahn 2010-08-31 changing order of premises generated when flattening functions in premises; adapting example for second attack for hotel key card system
2010-08-31 bulwahn 2010-08-31 added further hotel key card attack in example file
2010-08-31 bulwahn 2010-08-31 storing options for prolog code generation in the theory
2010-08-31 bulwahn 2010-08-31 adapting example files to latest changes
2010-08-25 bulwahn 2010-08-25 changing hotel trace definition; adding simple handling of numerals on natural numbers
2010-08-25 bulwahn 2010-08-25 added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
2010-08-25 bulwahn 2010-08-25 invocation of values for prolog execution does not require invocation of code_pred anymore
2010-08-25 bulwahn 2010-08-25 adding hotel keycard example for prolog generation