src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
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
Tue, 07 Sep 2010 12:04:34 +0200 nipkow merged
Tue, 07 Sep 2010 10:05:19 +0200 nipkow expand_fun_eq -> ext_iff
Tue, 07 Sep 2010 11:51:53 +0200 bulwahn adapting example files
Tue, 31 Aug 2010 15:21:56 +0200 bulwahn adapting and tuning example theories
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
Tue, 31 Aug 2010 08:00:55 +0200 bulwahn added further hotel key card attack in example file
Tue, 31 Aug 2010 08:00:53 +0200 bulwahn storing options for prolog code generation in the theory
Tue, 31 Aug 2010 08:00:52 +0200 bulwahn adapting example files to latest changes
Wed, 25 Aug 2010 16:59:53 +0200 bulwahn changing hotel trace definition; adding simple handling of numerals on natural numbers
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
Wed, 25 Aug 2010 16:59:50 +0200 bulwahn invocation of values for prolog execution does not require invocation of code_pred anymore
Wed, 25 Aug 2010 16:59:49 +0200 bulwahn adding hotel keycard example for prolog generation
less more (0) tip