Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Doc/Tutorial/CTL/PDL.thy
changeset 80983 2cc651d3ce8e
parent 80914 d97fdabd9e2b 
--- a/src/Doc/Tutorial/CTL/PDL.thy	Fri Sep 27 22:44:30 2024 +0200
+++ b/src/Doc/Tutorial/CTL/PDL.thy	Fri Sep 27 23:47:45 2024 +0200
@@ -26,7 +26,7 @@
 \hbox{\<open>valid s f\<close>}. The definition is by recursion over the syntax:
 \<close>
 
-primrec valid :: "state \<Rightarrow> formula \<Rightarrow> bool"   (\<open>(_ \<Turnstile> _)\<close> [80,80] 80)
+primrec valid :: "state \<Rightarrow> formula \<Rightarrow> bool"   ("(_ \<Turnstile> _)" [80,80] 80)
 where
 "s \<Turnstile> Atom a  = (a \<in> L s)" |
 "s \<Turnstile> Neg f   = (\<not>(s \<Turnstile> f))" |
isabelle