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/MicroJava/J/Eval.thy
changeset 28524 644b62cf678f
parent 23757 087b0a241557
child 33128 1f990689349f
child 35416 d8d7d1b785af 
--- a/src/HOL/MicroJava/J/Eval.thy	Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy	Tue Oct 07 16:07:50 2008 +0200
@@ -45,7 +45,7 @@
 
   -- "evaluation of expressions"
 
-  XcptE:"G\<turnstile>(Some xc,s) -e\<succ>arbitrary-> (Some xc,s)"  -- "cf. 15.5"
+  XcptE:"G\<turnstile>(Some xc,s) -e\<succ>undefined-> (Some xc,s)"  -- "cf. 15.5"
 
   -- "cf. 15.8.1"
 | NewC: "[| h = heap s; (a,x) = new_Addr h;
@@ -98,7 +98,7 @@
   -- "evaluation of expression lists"
 
   -- "cf. 15.5"
-| XcptEs:"G\<turnstile>(Some xc,s) -e[\<succ>]arbitrary-> (Some xc,s)"
+| XcptEs:"G\<turnstile>(Some xc,s) -e[\<succ>]undefined-> (Some xc,s)"
 
   -- "cf. 15.11.???"
 | Nil:  "G\<turnstile>Norm s0 -[][\<succ>][]-> Norm s0"
isabelle