equal
deleted
inserted
replaced
79 val ii = Fun (Input, Fun (Input, Bool)) |
79 val ii = Fun (Input, Fun (Input, Bool)) |
80 in |
80 in |
81 Core_Data.PredData.map (Graph.new_node |
81 Core_Data.PredData.map (Graph.new_node |
82 (@{const_name contains}, |
82 (@{const_name contains}, |
83 Core_Data.PredData { |
83 Core_Data.PredData { |
|
84 pos = Position.thread_data (), |
84 intros = [(NONE, @{thm containsI})], |
85 intros = [(NONE, @{thm containsI})], |
85 elim = SOME @{thm containsE}, |
86 elim = SOME @{thm containsE}, |
86 preprocessed = true, |
87 preprocessed = true, |
87 function_names = [(Predicate_Compile_Aux.Pred, |
88 function_names = [(Predicate_Compile_Aux.Pred, |
88 [(io, @{const_name pred_of_set}), (ii, @{const_name contains_pred})])], |
89 [(io, @{const_name pred_of_set}), (ii, @{const_name contains_pred})])], |