src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
changeset 38731 2c8a595af43e
parent 38730 5bbdd9a9df62
child 38733 4b8fd91ea59a
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Wed Aug 25 16:59:49 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Wed Aug 25 16:59:50 2010 +0200
     1.3 @@ -84,10 +84,10 @@
     1.4  lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
     1.5  by (auto simp add: Diff_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection)
     1.6  
     1.7 -code_pred [new_random_dseq inductify, skip_proof] hotel .
     1.8 -
     1.9  ML {* Code_Prolog.options := {ensure_groundness = true} *}
    1.10  
    1.11  values 10 "{s. hotel s}"
    1.12  
    1.13 +
    1.14 +
    1.15  end
    1.16 \ No newline at end of file