--- a/src/HOL/MicroJava/BV/LBVCorrect.thy Mon Oct 14 13:35:17 2002 +0200
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Tue Oct 15 15:37:57 2002 +0200
@@ -9,7 +9,7 @@
theory LBVCorrect = LBVSpec + Typing_Framework:
locale (open) lbvs = lbv +
- fixes s0 :: 'a
+ fixes s0 :: 'a ("s\<^sub>0")
fixes c :: "'a list"
fixes ins :: "'b list"
fixes phi :: "'a list" ("\<phi>")
@@ -36,9 +36,9 @@
lemma (in lbvs) wtl_suc_pc:
- assumes all: "wtl ins c 0 s0 \<noteq> \<top>"
+ assumes all: "wtl ins c 0 s\<^sub>0 \<noteq> \<top>"
assumes pc: "pc+1 < length ins"
- shows "wtl (take (pc+1) ins) c 0 s0 <=_r \<phi>!(pc+1)"
+ shows "wtl (take (pc+1) ins) c 0 s0 \<le>\<^sub>r \<phi>!(pc+1)"
proof -
from all pc
have "wtc c (pc+1) (wtl (take (pc+1) ins) c 0 s0) \<noteq> T" by (rule wtl_all)
--- a/src/HOL/MicroJava/BV/Semilat.thy Mon Oct 14 13:35:17 2002 +0200
+++ b/src/HOL/MicroJava/BV/Semilat.thy Tue Oct 15 15:37:57 2002 +0200
@@ -24,11 +24,20 @@
lesub_def: "x <=_r y == r x y"
lesssub_def: "x <_r y == x <=_r y & x ~= y"
+syntax (xsymbols)
+ "@lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<le>\<^sub>_ _)" [50, 1000, 51] 50)
+
consts
"@plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /+'__ _)" [65, 1000, 66] 65)
defs
plussub_def: "x +_f y == f x y"
+syntax (xsymbols)
+ "@plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /+\<^sub>_ _)" [65, 1000, 66] 65)
+
+syntax (xsymbols)
+ "@plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65)
+
constdefs
ord :: "('a*'a)set \<Rightarrow> 'a ord"