equal
deleted
inserted
replaced
23 EmptyList :: "bool list" |
23 EmptyList :: "bool list" |
24 UniversalList :: "bool list" |
24 UniversalList :: "bool list" |
25 |
25 |
26 ML \<open> |
26 ML \<open> |
27 \<close> ML \<open> |
27 \<close> ML \<open> |
28 val UniversalList = (Thm.term_of o the o (TermC.parse @{theory})) "UniversalList"; |
28 val UniversalList = TermC.parseNEW'' @{theory} "UniversalList"; |
29 val EmptyList = (Thm.term_of o the o (TermC.parse @{theory})) "[]::bool list"; |
29 val EmptyList = TermC.parseNEW'' @{theory} "[]::bool list"; |
30 \<close> ML \<open> |
30 \<close> ML \<open> |
31 \<close> |
31 \<close> |
32 |
32 |
33 subsection \<open>Type 'xlist' for Lucas-Interpretation | for InsSort.thy\<close> |
33 subsection \<open>Type 'xlist' for Lucas-Interpretation | for InsSort.thy\<close> |
34 (* cp fom ~~/src/HOL/List.thy |
34 (* cp fom ~~/src/HOL/List.thy |