# HG changeset patch
# User wenzelm
# Date 967830057 -7200
# Node ID 2c3d4e03e00c8b38613aa2046ab04808c792ec5b
# Parent  bbefb6ce5cb28801f1d6afe5f8c13f512374b4d8
isatool nonascii;

diff -r bbefb6ce5cb2 -r 2c3d4e03e00c src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Fri Sep 01 19:09:44 2000 +0200
+++ b/src/HOL/MicroJava/J/Example.thy	Fri Sep 01 19:40:57 2000 +0200
@@ -86,7 +86,7 @@
 			     [((foo,[Class Base]),Class Ext,foo_Ext)]))"
 
   test_def "test \\<equiv> Expr(e\\<Colon>=NewC Ext);; 
-		    Expr(LAcc e..foo({[Class Base]}[Lit Null]))"
+                    Expr(LAcc e..foo({[Class Base]}[Lit Null]))"
 
 
 syntax
@@ -102,8 +102,8 @@
   "tprg" == "[ObjectC, BaseC, ExtC]"
   "obj1"    <= "(Ext, empty((vee, Base)\\<mapsto>Bool False)
 			   ((vee, Ext )\\<mapsto>Intg #0))"
-  "s0" == " Norm    (empty          ,empty                        )"
-  "s1" == " Norm    (empty(a\\<mapsto>obj1),empty(e\\<mapsto>Addr a)             )"
+  "s0" == " Norm    (empty, empty)"
+  "s1" == " Norm    (empty(a\\<mapsto>obj1),empty(e\\<mapsto>Addr a))"
   "s2" == " Norm    (empty(a\\<mapsto>obj1),empty(x\\<mapsto>Null)(This\\<mapsto>Addr a))"
   "s3" == "(Some NP, empty(a\\<mapsto>obj1),empty(e\\<mapsto>Addr a))"
 end