# HG changeset patch
# User kleing
# Date 1034689077 -7200
# Node ID 0f562a70c07dc430af57bd155e8b4bc2c0d2987c
# Parent  610cedff553889ebb860fbae12abebf69b9dc8a1
alternative syntax

diff -r 610cedff5538 -r 0f562a70c07d src/HOL/MicroJava/BV/LBVCorrect.thy
--- 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)
diff -r 610cedff5538 -r 0f562a70c07d src/HOL/MicroJava/BV/Semilat.thy
--- 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"