src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
changeset 38950 62578950e748
parent 38949 1afa9e89c885
child 38953 0c38eb5fc4ca
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Aug 31 08:00:52 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Aug 31 08:00:53 2010 +0200
     1.3 @@ -84,12 +84,12 @@
     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 -ML {* Code_Prolog.options :=
     1.8 +setup {* Code_Prolog.map_code_options (K
     1.9    {ensure_groundness = true,
    1.10    limited_types = [],
    1.11    limited_predicates = [],
    1.12    replacing = [],
    1.13 -  prolog_system = Code_Prolog.SWI_PROLOG} *}
    1.14 +  prolog_system = Code_Prolog.SWI_PROLOG}) *}
    1.15  
    1.16  values 40 "{s. hotel s}"
    1.17