--- a/src/HOL/Bali/Eval.thy Tue Feb 09 16:07:09 2010 +0100
+++ b/src/HOL/Bali/Eval.thy Wed Feb 10 00:45:16 2010 +0100
@@ -125,20 +125,21 @@
assignment.
*}
-syntax (xsymbols)
+abbreviation (xsymbols)
dummy_res :: "vals" ("\<diamondsuit>")
-translations
- "\<diamondsuit>" == "In1 Unit"
+ where "\<diamondsuit> == In1 Unit"
+
+abbreviation (input)
+ val_inj_vals ("\<lfloor>_\<rfloor>\<^sub>e" 1000)
+ where "\<lfloor>e\<rfloor>\<^sub>e == In1 e"
-syntax
- val_inj_vals:: "expr \<Rightarrow> term" ("\<lfloor>_\<rfloor>\<^sub>e" 1000)
- var_inj_vals:: "var \<Rightarrow> term" ("\<lfloor>_\<rfloor>\<^sub>v" 1000)
- lst_inj_vals:: "expr list \<Rightarrow> term" ("\<lfloor>_\<rfloor>\<^sub>l" 1000)
+abbreviation (input)
+ var_inj_vals ("\<lfloor>_\<rfloor>\<^sub>v" 1000)
+ where "\<lfloor>v\<rfloor>\<^sub>v == In2 v"
-translations
- "\<lfloor>e\<rfloor>\<^sub>e" \<rightharpoonup> "In1 e"
- "\<lfloor>v\<rfloor>\<^sub>v" \<rightharpoonup> "In2 v"
- "\<lfloor>es\<rfloor>\<^sub>l" \<rightharpoonup> "In3 es"
+abbreviation (input)
+ lst_inj_vals ("\<lfloor>_\<rfloor>\<^sub>l" 1000)
+ where "\<lfloor>es\<rfloor>\<^sub>l == In3 es"
constdefs
undefined3 :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> vals"