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/HOL/ex/CodeEmbed.thy
changeset 21404 eb85850d3eb7
parent 21113 5b76e541cc0a
child 21455 b6be1d1b66c5 
--- a/src/HOL/ex/CodeEmbed.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/ex/CodeEmbed.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -22,9 +22,10 @@
   | TFix vname sort (infix "\<Colon>\<epsilon>" 117)
 
 abbreviation
-  Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" (infixr "\<rightarrow>" 115)
+  Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" (infixr "\<rightarrow>" 115) where
   "ty1 \<rightarrow> ty2 \<equiv> Type (STR ''fun'') [ty1, ty2]"
-  Funs :: "typ list \<Rightarrow> typ \<Rightarrow> typ" (infixr "{\<rightarrow>}" 115)
+abbreviation
+  Funs :: "typ list \<Rightarrow> typ \<Rightarrow> typ" (infixr "{\<rightarrow>}" 115) where
   "tys {\<rightarrow>} ty \<equiv> foldr (op \<rightarrow>) tys ty"
 
 datatype "term" =
@@ -33,7 +34,7 @@
   | App   "term" "term" (infixl "\<bullet>" 110)
 
 abbreviation
-  Apps :: "term \<Rightarrow> term list \<Rightarrow> term"  (infixl "{\<bullet>}" 110)
+  Apps :: "term \<Rightarrow> term list \<Rightarrow> term"  (infixl "{\<bullet>}" 110) where
   "t {\<bullet>} ts \<equiv> foldl (op \<bullet>) t ts"
isabelle