src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy

 where
   "\<not> ck \<Longrightarrow> ck = False \<Longrightarrow> predicate_where_argument_is_neg_condition_and_in_equation ck"
 
 code_pred predicate_where_argument_is_neg_condition_and_in_equation .
 
-text {* Another related example that required slight adjustment of the proof procedure *}
+text \<open>Another related example that required slight adjustment of the proof procedure\<close>
 
 inductive if_as_predicate :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
 where
   "condition \<Longrightarrow> if_as_predicate condition then_value else_value then_value"
 | "\<not> condition \<Longrightarrow> if_as_predicate condition then_value else_value else_value"