--- a/src/HOL/MicroJava/J/State.thy Wed Feb 10 23:53:46 2010 +0100
+++ b/src/HOL/MicroJava/J/State.thy Thu Feb 11 00:45:02 2010 +0100
@@ -27,21 +27,27 @@
state = "aheap \<times> locals" -- "heap, local parameter including This"
xstate = "val option \<times> state" -- "state including exception information"
-syntax
- heap :: "state => aheap"
- locals :: "state => locals"
- Norm :: "state => xstate"
- abrupt :: "xstate \<Rightarrow> val option"
- store :: "xstate \<Rightarrow> state"
- lookup_obj :: "state \<Rightarrow> val \<Rightarrow> obj"
+abbreviation (input)
+ heap :: "state => aheap"
+ where "heap == fst"
+
+abbreviation (input)
+ locals :: "state => locals"
+ where "locals == snd"
+
+abbreviation "Norm s == (None, s)"
-translations
- "heap" => "fst"
- "locals" => "snd"
- "Norm s" == "(None,s)"
- "abrupt" => "fst"
- "store" => "snd"
- "lookup_obj s a'" == "CONST the (heap s (the_Addr a'))"
+abbreviation (input)
+ abrupt :: "xstate \<Rightarrow> val option"
+ where "abrupt == fst"
+
+abbreviation (input)
+ store :: "xstate \<Rightarrow> state"
+ where "store == snd"
+
+abbreviation
+ lookup_obj :: "state \<Rightarrow> val \<Rightarrow> obj"
+ where "lookup_obj s a' == the (heap s (the_Addr a'))"
constdefs