--- a/src/HOL/Bali/State.thy Sun Oct 27 12:54:58 2024 +0100
+++ b/src/HOL/Bali/State.thy Sun Oct 27 15:30:00 2024 +0100
@@ -131,19 +131,15 @@
subsubsection "object references"
type_synonym oref = "loc + qtname" \<comment> \<open>generalized object reference\<close>
-syntax
- Heap :: "loc \<Rightarrow> oref"
- Stat :: "qtname \<Rightarrow> oref"
-
-syntax_consts
- Heap == Inl and
- Stat == Inr
translations
- "Heap" => "CONST Inl"
- "Stat" => "CONST Inr"
(type) "oref" <= (type) "loc + qtname"
+abbreviation (input)
+ Heap :: "loc \<Rightarrow> oref" where "Heap \<equiv> Inl"
+abbreviation (input)
+ Stat :: "qtname \<Rightarrow> oref" where "Stat \<equiv> Inr"
+
definition
fields_table :: "prog \<Rightarrow> qtname \<Rightarrow> (fspec \<Rightarrow> field \<Rightarrow> bool) \<Rightarrow> (fspec, ty) table" where
"fields_table G C P =