equal
deleted
inserted
replaced
8 |
8 |
9 theory Metis |
9 theory Metis |
10 imports ATP |
10 imports ATP |
11 begin |
11 begin |
12 |
12 |
13 ML_file \<open>~~/src/Tools/Metis/metis.ML\<close> |
13 context notes [[ML_catch_all]] |
|
14 begin |
|
15 ML_file \<open>~~/src/Tools/Metis/metis.ML\<close> |
|
16 end |
14 |
17 |
15 |
18 |
16 subsection \<open>Literal selection and lambda-lifting helpers\<close> |
19 subsection \<open>Literal selection and lambda-lifting helpers\<close> |
17 |
20 |
18 definition select :: "'a \<Rightarrow> 'a" where |
21 definition select :: "'a \<Rightarrow> 'a" where |