78 val Bool = Predicate_Compile_Aux.Bool |
78 val Bool = Predicate_Compile_Aux.Bool |
79 val io = Fun (Input, Fun (Output, Bool)) |
79 val io = Fun (Input, Fun (Output, Bool)) |
80 val ii = Fun (Input, Fun (Input, Bool)) |
80 val ii = Fun (Input, Fun (Input, Bool)) |
81 in |
81 in |
82 Core_Data.PredData.map (Graph.new_node |
82 Core_Data.PredData.map (Graph.new_node |
83 (@{const_name contains}, |
83 (\<^const_name>\<open>contains\<close>, |
84 Core_Data.PredData { |
84 Core_Data.PredData { |
85 pos = Position.thread_data (), |
85 pos = Position.thread_data (), |
86 intros = [(NONE, @{thm containsI})], |
86 intros = [(NONE, @{thm containsI})], |
87 elim = SOME @{thm containsE}, |
87 elim = SOME @{thm containsE}, |
88 preprocessed = true, |
88 preprocessed = true, |
89 function_names = [(Predicate_Compile_Aux.Pred, |
89 function_names = [(Predicate_Compile_Aux.Pred, |
90 [(io, @{const_name pred_of_set}), (ii, @{const_name contains_pred})])], |
90 [(io, \<^const_name>\<open>pred_of_set\<close>), (ii, \<^const_name>\<open>contains_pred\<close>)])], |
91 predfun_data = [ |
91 predfun_data = [ |
92 (io, Core_Data.PredfunData { |
92 (io, Core_Data.PredfunData { |
93 elim = @{thm pred_of_setE}, intro = @{thm pred_of_setI}, |
93 elim = @{thm pred_of_setE}, intro = @{thm pred_of_setI}, |
94 neg_intro = NONE, definition = @{thm pred_of_set_eq} |
94 neg_intro = NONE, definition = @{thm pred_of_set_eq} |
95 }), |
95 }), |