# HG changeset patch
# User nipkow
# Date 1059146482 -7200
# Node ID 0fdf5708c7a8041ada982ea3da52b2d7712dfcb6
# Parent  4cd1a7e7edac528e6d4427285e1835ce0046a662
Replaced \<leadsto> by \<rightharpoonup>

diff -r 4cd1a7e7edac -r 0fdf5708c7a8 src/HOL/Bali/Table.thy
--- 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]:
diff -r 4cd1a7e7edac -r 0fdf5708c7a8 src/HOL/Map.thy
--- 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)
diff -r 4cd1a7e7edac -r 0fdf5708c7a8 src/HOL/MicroJava/J/Conform.thy
--- 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"
diff -r 4cd1a7e7edac -r 0fdf5708c7a8 src/HOL/MicroJava/J/Decl.thy
--- 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"
diff -r 4cd1a7e7edac -r 0fdf5708c7a8 src/HOL/MicroJava/J/State.thy
--- 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"
diff -r 4cd1a7e7edac -r 0fdf5708c7a8 src/HOL/MicroJava/J/TypeRel.thy
--- 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"
diff -r 4cd1a7e7edac -r 0fdf5708c7a8 src/HOL/MicroJava/J/WellType.thy
--- 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"
diff -r 4cd1a7e7edac -r 0fdf5708c7a8 src/HOL/NanoJava/Decl.thy
--- 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"
diff -r 4cd1a7e7edac -r 0fdf5708c7a8 src/HOL/NanoJava/State.thy
--- 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
diff -r 4cd1a7e7edac -r 0fdf5708c7a8 src/HOL/NanoJava/TypeRel.thy
--- 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