--- a/src/HOL/Bali/Table.thy Fri Jul 25 10:52:15 2003 +0200
+++ b/src/HOL/Bali/Table.thy Fri Jul 25 17:21:22 2003 +0200
@@ -32,7 +32,7 @@
*}
types ('a, 'b) table --{* table with key type 'a and contents type 'b *}
- = "'a \<leadsto> 'b"
+ = "'a \<rightharpoonup> 'b"
('a, 'b) tables --{* non-unique table with key 'a and contents 'b *}
= "'a \<Rightarrow> 'b set"
@@ -45,8 +45,8 @@
translations
"table_of" == "map_of"
- (type)"'a \<leadsto> 'b" <= (type)"'a \<Rightarrow> 'b Option.option"
- (type)"('a, 'b) table" <= (type)"'a \<leadsto> 'b"
+ (type)"'a \<rightharpoonup> 'b" <= (type)"'a \<Rightarrow> 'b Option.option"
+ (type)"('a, 'b) table" <= (type)"'a \<rightharpoonup> 'b"
(* ### To map *)
lemma map_add_find_left[simp]:
--- a/src/HOL/Map.thy Fri Jul 25 10:52:15 2003 +0200
+++ b/src/HOL/Map.thy Fri Jul 25 17:21:22 2003 +0200
@@ -35,7 +35,7 @@
("_/'(_/|->_')" [900,0,0]900)
syntax (xsymbols)
- "~=>" :: "[type, type] => type" (infixr "\<leadsto>" 0)
+ "~=>" :: "[type, type] => type" (infixr "\<rightharpoonup>" 0)
restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" ("_\<lfloor>_" [90, 91] 90)
map_upd :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
("_/'(_/\<mapsto>/_')" [900,0,0]900)
--- a/src/HOL/MicroJava/J/Conform.thy Fri Jul 25 10:52:15 2003 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy Fri Jul 25 17:21:22 2003 +0200
@@ -8,7 +8,7 @@
theory Conform = State + WellType + Exceptions:
-types 'c env_ = "'c prog \<times> (vname \<leadsto> ty)" -- "same as @{text env} of @{text WellType.thy}"
+types 'c env_ = "'c prog \<times> (vname \<rightharpoonup> ty)" -- "same as @{text env} of @{text WellType.thy}"
constdefs
@@ -19,7 +19,7 @@
("_,_ |- _ ::<= _" [51,51,51,51] 50)
"G,h|-v::<=T == \<exists>T'. typeof (option_map obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T"
- lconf :: "'c prog => aheap => ('a \<leadsto> val) => ('a \<leadsto> ty) => bool"
+ lconf :: "'c prog => aheap => ('a \<rightharpoonup> val) => ('a \<rightharpoonup> ty) => bool"
("_,_ |- _ [::<=] _" [51,51,51,51] 50)
"G,h|-vs[::<=]Ts == \<forall>n T. Ts n = Some T --> (\<exists>v. vs n = Some v \<and> G,h|-v::<=T)"
@@ -45,7 +45,7 @@
conf :: "'c prog => aheap => val => ty => bool"
("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50)
- lconf :: "'c prog => aheap => ('a \<leadsto> val) => ('a \<leadsto> ty) => bool"
+ lconf :: "'c prog => aheap => ('a \<rightharpoonup> val) => ('a \<rightharpoonup> ty) => bool"
("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50)
oconf :: "'c prog => aheap => obj => bool"
--- a/src/HOL/MicroJava/J/Decl.thy Fri Jul 25 10:52:15 2003 +0200
+++ b/src/HOL/MicroJava/J/Decl.thy Fri Jul 25 17:21:22 2003 +0200
@@ -33,7 +33,7 @@
constdefs
- class :: "'c prog => (cname \<leadsto> 'c class)"
+ class :: "'c prog => (cname \<rightharpoonup> 'c class)"
"class \<equiv> map_of"
is_class :: "'c prog => cname => bool"
--- a/src/HOL/MicroJava/J/State.thy Fri Jul 25 10:52:15 2003 +0200
+++ b/src/HOL/MicroJava/J/State.thy Fri Jul 25 17:21:22 2003 +0200
@@ -9,7 +9,7 @@
theory State = TypeRel + Value:
types
- fields_ = "(vname \<times> cname \<leadsto> val)" -- "field name, defining class, value"
+ fields_ = "(vname \<times> cname \<rightharpoonup> val)" -- "field name, defining class, value"
obj = "cname \<times> fields_" -- "class instance with class name and fields"
@@ -17,12 +17,12 @@
obj_ty :: "obj => ty"
"obj_ty obj == Class (fst obj)"
- init_vars :: "('a \<times> ty) list => ('a \<leadsto> val)"
+ init_vars :: "('a \<times> ty) list => ('a \<rightharpoonup> val)"
"init_vars == map_of o map (\<lambda>(n,T). (n,default_val T))"
-types aheap = "loc \<leadsto> obj" -- {* "@{text heap}" used in a translation below *}
- locals = "vname \<leadsto> val" -- "simple state, i.e. variable contents"
+types aheap = "loc \<rightharpoonup> obj" -- {* "@{text heap}" used in a translation below *}
+ locals = "vname \<rightharpoonup> val" -- "simple state, i.e. variable contents"
state = "aheap \<times> locals" -- "heap, local parameter including This"
xstate = "val option \<times> state" -- "state including exception information"
--- a/src/HOL/MicroJava/J/TypeRel.thy Fri Jul 25 10:52:15 2003 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy Fri Jul 25 17:21:22 2003 +0200
@@ -81,8 +81,8 @@
consts
- method :: "'c prog \<times> cname => ( sig \<leadsto> cname \<times> ty \<times> 'c)" (* ###curry *)
- field :: "'c prog \<times> cname => ( vname \<leadsto> cname \<times> ty )" (* ###curry *)
+ method :: "'c prog \<times> cname => ( sig \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
+ field :: "'c prog \<times> cname => ( vname \<rightharpoonup> cname \<times> ty )" (* ###curry *)
fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *)
-- "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6"
--- a/src/HOL/MicroJava/J/WellType.thy Fri Jul 25 10:52:15 2003 +0200
+++ b/src/HOL/MicroJava/J/WellType.thy Fri Jul 25 17:21:22 2003 +0200
@@ -24,12 +24,12 @@
text "local variables, including method parameters and This:"
types
- lenv = "vname \<leadsto> ty"
+ lenv = "vname \<rightharpoonup> ty"
'c env = "'c prog \<times> lenv"
syntax
prg :: "'c env => 'c prog"
- localT :: "'c env => (vname \<leadsto> ty)"
+ localT :: "'c env => (vname \<rightharpoonup> ty)"
translations
"prg" => "fst"
--- a/src/HOL/NanoJava/Decl.thy Fri Jul 25 10:52:15 2003 +0200
+++ b/src/HOL/NanoJava/Decl.thy Fri Jul 25 17:21:22 2003 +0200
@@ -52,7 +52,7 @@
constdefs
- class :: "cname \<leadsto> class"
+ class :: "cname \<rightharpoonup> class"
"class \<equiv> map_of Prog"
is_class :: "cname => bool"
--- a/src/HOL/NanoJava/State.thy Fri Jul 25 10:52:15 2003 +0200
+++ b/src/HOL/NanoJava/State.thy Fri Jul 25 17:21:22 2003 +0200
@@ -21,7 +21,7 @@
| Addr loc --{* address, i.e. location of object *}
types fields
- = "(fname \<leadsto> val)"
+ = "(fname \<rightharpoonup> val)"
obj = "cname \<times> fields"
@@ -32,12 +32,12 @@
constdefs
- init_vars:: "('a \<leadsto> 'b) => ('a \<leadsto> val)"
+ init_vars:: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> val)"
"init_vars m == option_map (\<lambda>T. Null) o m"
text {* private: *}
-types heap = "loc \<leadsto> obj"
- locals = "vname \<leadsto> val"
+types heap = "loc \<rightharpoonup> obj"
+ locals = "vname \<rightharpoonup> val"
text {* private: *}
record state
--- a/src/HOL/NanoJava/TypeRel.thy Fri Jul 25 10:52:15 2003 +0200
+++ b/src/HOL/NanoJava/TypeRel.thy Fri Jul 25 17:21:22 2003 +0200
@@ -27,8 +27,8 @@
"S \<preceq> T" == "(S,T) \<in> widen"
consts
- method :: "cname => (mname \<leadsto> methd)"
- field :: "cname => (fname \<leadsto> ty)"
+ method :: "cname => (mname \<rightharpoonup> methd)"
+ field :: "cname => (fname \<rightharpoonup> ty)"
subsection "Declarations and properties not used in the meta theory"
@@ -102,7 +102,7 @@
by (auto intro: finite_acyclic_wf_converse finite_subcls1 subcls1_acyclic)
-consts class_rec ::"cname \<Rightarrow> (class \<Rightarrow> ('a \<times> 'b) list) \<Rightarrow> ('a \<leadsto> 'b)"
+consts class_rec ::"cname \<Rightarrow> (class \<Rightarrow> ('a \<times> 'b) list) \<Rightarrow> ('a \<rightharpoonup> 'b)"
recdef (permissive) class_rec "subcls1\<inverse>"
"class_rec C = (\<lambda>f. case class C of None \<Rightarrow> arbitrary