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/Lambda/Type.thy
changeset 19363 667b5ea637dd
parent 19086 1b3780be6cc2
child 19380 b808efaa5828 
--- a/src/HOL/Lambda/Type.thy	Sat Apr 08 22:12:02 2006 +0200
+++ b/src/HOL/Lambda/Type.thy	Sat Apr 08 22:51:06 2006 +0200
@@ -14,10 +14,14 @@
 definition
   shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_<_:_>" [90, 0, 0] 91)
   "e<i:a> = (\<lambda>j. if j < i then e j else if j = i then a else e (j - 1))"
-syntax (xsymbols)
-  shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
-syntax (HTML output)
-  shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
+
+abbreviation (xsymbols)
+  shift  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
+  "e\<langle>i:a\<rangle> == e<i:a>"
+
+abbreviation (HTML output)
+  shift  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
+  "shift == xsymbols.shift"
 
 lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T"
   by (simp add: shift_def)
@@ -47,23 +51,27 @@
   typing :: "((nat \<Rightarrow> type) \<times> dB \<times> type) set"
   typings :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
 
-abbreviation (output)
+abbreviation
   funs :: "type list \<Rightarrow> type \<Rightarrow> type"    (infixr "=>>" 200)
-  "Ts =>> T = foldr Fun Ts T"
+  "Ts =>> T == foldr Fun Ts T"
 
   typing_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ |- _ : _" [50, 50, 50] 50)
-  "(env |- t : T) = ((env, t, T) \<in> typing)"
+  "env |- t : T == (env, t, T) \<in> typing"
 
   typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
     ("_ ||- _ : _" [50, 50, 50] 50)
-  "(env ||- ts : Ts) = typings env ts Ts"
+  "env ||- ts : Ts == typings env ts Ts"
 
-syntax (xsymbols)
+abbreviation (xsymbols)
   typing_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile> _ : _" [50, 50, 50] 50)
-syntax (latex)
+  "env \<turnstile> t : T == env |- t : T"
+
+abbreviation (latex)
   funs :: "type list \<Rightarrow> type \<Rightarrow> type"    (infixr "\<Rrightarrow>" 200)
+  "op \<Rrightarrow> == op =>>"
   typings_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB list \<Rightarrow> type list \<Rightarrow> bool"
     ("_ \<tturnstile> _ : _" [50, 50, 50] 50)
+  "env \<tturnstile> ts : Ts == env ||- ts : Ts"
 
 inductive typing
   intros
isabelle