changeset 69587 | 53982d5ec0bb |
parent 62020 | 5d208fd2507d |
child 69590 | e65314985426 |
--- a/src/FOL/ex/Prolog.thy Thu Jan 03 21:06:39 2019 +0100 +++ b/src/FOL/ex/Prolog.thy Thu Jan 03 21:15:52 2019 +0100 @@ -14,7 +14,7 @@ axiomatization Nil :: "'a list" and - Cons :: "['a, 'a list]=> 'a list" (infixr ":" 60) and + Cons :: "['a, 'a list]=> 'a list" (infixr \<open>:\<close> 60) and app :: "['a list, 'a list, 'a list] => o" and rev :: "['a list, 'a list] => o" where