equal
deleted
inserted
replaced
81 lemma wf_in_rel: |
81 lemma wf_in_rel: |
82 "wf R \<Longrightarrow> wfP (in_rel R)" |
82 "wf R \<Longrightarrow> wfP (in_rel R)" |
83 by (simp add: wfP_def) |
83 by (simp add: wfP_def) |
84 |
84 |
85 ML_file "Tools/Function/function_core.ML" |
85 ML_file "Tools/Function/function_core.ML" |
86 ML_file "Tools/Function/sum_tree.ML" |
|
87 ML_file "Tools/Function/mutual.ML" |
86 ML_file "Tools/Function/mutual.ML" |
88 ML_file "Tools/Function/pattern_split.ML" |
87 ML_file "Tools/Function/pattern_split.ML" |
89 ML_file "Tools/Function/relation.ML" |
88 ML_file "Tools/Function/relation.ML" |
90 ML_file "Tools/Function/function_elims.ML" |
89 ML_file "Tools/Function/function_elims.ML" |
91 |
90 |