diff -r 1c8de414b45d -r 381716a86fcb src/HOL/MicroJava/J/Conform.thy --- a/src/HOL/MicroJava/J/Conform.thy Thu Dec 23 19:59:50 1999 +0100 +++ b/src/HOL/MicroJava/J/Conform.thy Mon Jan 03 14:07:08 2000 +0100 @@ -26,7 +26,7 @@ hconf :: "'c prog \\ aheap \\ bool" ("_\\h _\\" [51,51] 50) "G\\h h\\ \\ \\a obj. h a = Some obj \\ G,h\\obj\\" - conforms :: "state \\ javam env \\ bool" ("_\\\\_" [51,51] 50) + conforms :: "state \\ java_mb env \\ bool" ("_\\\\_" [51,51] 50) "s\\\\E \\ prg E\\h heap s\\ \\ prg E,heap s\\locals s[\\\\]localT E" end