equal
deleted
inserted
replaced
83 thus ?thesis |
83 thus ?thesis |
84 unfolding f_def |
84 unfolding f_def |
85 by (rule THE_default_none) |
85 by (rule THE_default_none) |
86 qed |
86 qed |
87 |
87 |
|
88 definition in_rel_def[simp]: |
|
89 "in_rel R x y == (x, y) \<in> R" |
|
90 |
|
91 lemma wf_in_rel: |
|
92 "wf R \<Longrightarrow> wfP (in_rel R)" |
|
93 by (simp add: wfP_def) |
|
94 |
|
95 |
88 use "Tools/function_package/fundef_lib.ML" |
96 use "Tools/function_package/fundef_lib.ML" |
89 use "Tools/function_package/fundef_common.ML" |
97 use "Tools/function_package/fundef_common.ML" |
90 use "Tools/function_package/inductive_wrap.ML" |
98 use "Tools/function_package/inductive_wrap.ML" |
91 use "Tools/function_package/context_tree.ML" |
99 use "Tools/function_package/context_tree.ML" |
92 use "Tools/function_package/fundef_core.ML" |
100 use "Tools/function_package/fundef_core.ML" |