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/CCL/Term.thy
changeset 80914 d97fdabd9e2b
parent 80761 bc936d3d8b45
child 80917 2a77bc3b4eac 
--- a/src/CCL/Term.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/CCL/Term.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -12,7 +12,7 @@
 definition one :: "i"
   where "one == true"
 
-definition "if" :: "[i,i,i]\<Rightarrow>i"  ("(3if _/ then _/ else _)" [0,0,60] 60)
+definition "if" :: "[i,i,i]\<Rightarrow>i"  (\<open>(3if _/ then _/ else _)\<close> [0,0,60] 60)
   where "if b then t else u  == case(b, t, u, \<lambda> x y. bot, \<lambda>v. bot)"
 
 definition inl :: "i\<Rightarrow>i"
@@ -48,7 +48,7 @@
 definition "let1" :: "[i,i\<Rightarrow>i]\<Rightarrow>i"
   where let_def: "let1(t, f) == case(t,f(true),f(false), \<lambda>x y. f(<x,y>), \<lambda>u. f(lam x. u(x)))"
 
-syntax "_let1" :: "[idt,i,i]\<Rightarrow>i"  ("(3let _ be _/ in _)" [0,0,60] 60)
+syntax "_let1" :: "[idt,i,i]\<Rightarrow>i"  (\<open>(3let _ be _/ in _)\<close> [0,0,60] 60)
 syntax_consts "_let1" == let1
 translations "let x be a in e" == "CONST let1(a, \<lambda>x. e)"
 
@@ -65,9 +65,9 @@
       \<lambda>g'. f(\<lambda>x y z. g'(<x,<y,z>>)))"
 
 syntax
-  "_letrec" :: "[idt,idt,i,i]\<Rightarrow>i"  ("(3letrec _ _ be _/ in _)" [0,0,0,60] 60)
-  "_letrec2" :: "[idt,idt,idt,i,i]\<Rightarrow>i"  ("(3letrec _ _ _ be _/ in _)" [0,0,0,0,60] 60)
-  "_letrec3" :: "[idt,idt,idt,idt,i,i]\<Rightarrow>i"  ("(3letrec _ _ _ _ be _/ in _)" [0,0,0,0,0,60] 60)
+  "_letrec" :: "[idt,idt,i,i]\<Rightarrow>i"  (\<open>(3letrec _ _ be _/ in _)\<close> [0,0,0,60] 60)
+  "_letrec2" :: "[idt,idt,idt,i,i]\<Rightarrow>i"  (\<open>(3letrec _ _ _ be _/ in _)\<close> [0,0,0,0,60] 60)
+  "_letrec3" :: "[idt,idt,idt,idt,i,i]\<Rightarrow>i"  (\<open>(3letrec _ _ _ _ be _/ in _)\<close> [0,0,0,0,0,60] 60)
 syntax_consts
   "_letrec" == letrec and
   "_letrec2" == letrec2 and
@@ -131,10 +131,10 @@
 definition nrec :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
   where "nrec(n,b,c) == letrec g x be ncase(x, b, \<lambda>y. c(y,g(y))) in g(n)"
 
-definition nil :: "i"  ("([])")
+definition nil :: "i"  (\<open>([])\<close>)
   where "[] == inl(one)"
 
-definition cons :: "[i,i]\<Rightarrow>i"  (infixr "$" 80)
+definition cons :: "[i,i]\<Rightarrow>i"  (infixr \<open>$\<close> 80)
   where "h$t == inr(<h,t>)"
 
 definition lcase :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
@@ -143,7 +143,7 @@
 definition lrec :: "[i,i,[i,i,i]\<Rightarrow>i]\<Rightarrow>i"
   where "lrec(l,b,c) == letrec g x be lcase(x, b, \<lambda>h t. c(h,t,g(t))) in g(l)"
 
-definition napply :: "[i\<Rightarrow>i,i,i]\<Rightarrow>i"  ("(_ ^ _ ` _)" [56,56,56] 56)
+definition napply :: "[i\<Rightarrow>i,i,i]\<Rightarrow>i"  (\<open>(_ ^ _ ` _)\<close> [56,56,56] 56)
   where "f ^n` a == nrec(n,a,\<lambda>x g. f(g))"
 
 lemmas simp_can_defs = one_def inl_def inr_def
isabelle