changeset 80914 | d97fdabd9e2b |
parent 68386 | 98cf1c823c48 |
child 82691 | b69e4da2604b |
--- a/src/HOL/MicroJava/DFA/LBVComplete.thy Fri Sep 20 19:07:10 2024 +0200 +++ b/src/HOL/MicroJava/DFA/LBVComplete.thy Fri Sep 20 19:51:08 2024 +0200 @@ -24,7 +24,7 @@ locale lbvc = lbv + - fixes phi :: "'a list" ("\<phi>") + fixes phi :: "'a list" (\<open>\<phi>\<close>) fixes c :: "'a list" defines cert_def: "c \<equiv> make_cert step \<phi> \<bottom>"