Replaced \<leadsto> by \<rightharpoonup>
authornipkow
Fri Jul 25 17:21:22 2003 +0200 (2003-07-25)
changeset 141340fdf5708c7a8
parent 14133 4cd1a7e7edac
child 14135 f8a25218b423
Replaced \<leadsto> by \<rightharpoonup>
src/HOL/Bali/Table.thy
src/HOL/Map.thy
src/HOL/MicroJava/J/Conform.thy
src/HOL/MicroJava/J/Decl.thy
src/HOL/MicroJava/J/State.thy
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/MicroJava/J/WellType.thy
src/HOL/NanoJava/Decl.thy
src/HOL/NanoJava/State.thy
src/HOL/NanoJava/TypeRel.thy
     1.1 --- a/src/HOL/Bali/Table.thy	Fri Jul 25 10:52:15 2003 +0200
     1.2 +++ b/src/HOL/Bali/Table.thy	Fri Jul 25 17:21:22 2003 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4  *}
     1.5  
     1.6  types ('a, 'b) table    --{* table with key type 'a and contents type 'b *}
     1.7 -      = "'a \<leadsto> 'b"
     1.8 +      = "'a \<rightharpoonup> 'b"
     1.9        ('a, 'b) tables   --{* non-unique table with key 'a and contents 'b *}
    1.10        = "'a \<Rightarrow> 'b set"
    1.11  
    1.12 @@ -45,8 +45,8 @@
    1.13  translations
    1.14    "table_of" == "map_of"
    1.15    
    1.16 -  (type)"'a \<leadsto> 'b"       <= (type)"'a \<Rightarrow> 'b Option.option"
    1.17 -  (type)"('a, 'b) table" <= (type)"'a \<leadsto> 'b"
    1.18 +  (type)"'a \<rightharpoonup> 'b"       <= (type)"'a \<Rightarrow> 'b Option.option"
    1.19 +  (type)"('a, 'b) table" <= (type)"'a \<rightharpoonup> 'b"
    1.20  
    1.21  (* ### To map *)
    1.22  lemma map_add_find_left[simp]:
     2.1 --- a/src/HOL/Map.thy	Fri Jul 25 10:52:15 2003 +0200
     2.2 +++ b/src/HOL/Map.thy	Fri Jul 25 17:21:22 2003 +0200
     2.3 @@ -35,7 +35,7 @@
     2.4  					 ("_/'(_/|->_')"   [900,0,0]900)
     2.5  
     2.6  syntax (xsymbols)
     2.7 -  "~=>"     :: "[type, type] => type"    (infixr "\<leadsto>" 0)
     2.8 +  "~=>"     :: "[type, type] => type"    (infixr "\<rightharpoonup>" 0)
     2.9    restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" ("_\<lfloor>_" [90, 91] 90)
    2.10    map_upd   :: "('a ~=> 'b) => 'a      => 'b      => ('a ~=> 'b)"
    2.11  					  ("_/'(_/\<mapsto>/_')"  [900,0,0]900)
     3.1 --- a/src/HOL/MicroJava/J/Conform.thy	Fri Jul 25 10:52:15 2003 +0200
     3.2 +++ b/src/HOL/MicroJava/J/Conform.thy	Fri Jul 25 17:21:22 2003 +0200
     3.3 @@ -8,7 +8,7 @@
     3.4  
     3.5  theory Conform = State + WellType + Exceptions:
     3.6  
     3.7 -types 'c env_ = "'c prog \<times> (vname \<leadsto> ty)"  -- "same as @{text env} of @{text WellType.thy}"
     3.8 +types 'c env_ = "'c prog \<times> (vname \<rightharpoonup> ty)"  -- "same as @{text env} of @{text WellType.thy}"
     3.9  
    3.10  constdefs
    3.11  
    3.12 @@ -19,7 +19,7 @@
    3.13                                     ("_,_ |- _ ::<= _"  [51,51,51,51] 50)
    3.14   "G,h|-v::<=T == \<exists>T'. typeof (option_map obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T"
    3.15  
    3.16 -  lconf :: "'c prog => aheap => ('a \<leadsto> val) => ('a \<leadsto> ty) => bool"
    3.17 +  lconf :: "'c prog => aheap => ('a \<rightharpoonup> val) => ('a \<rightharpoonup> ty) => bool"
    3.18                                     ("_,_ |- _ [::<=] _" [51,51,51,51] 50)
    3.19   "G,h|-vs[::<=]Ts == \<forall>n T. Ts n = Some T --> (\<exists>v. vs n = Some v \<and> G,h|-v::<=T)"
    3.20  
    3.21 @@ -45,7 +45,7 @@
    3.22    conf     :: "'c prog => aheap => val => ty => bool"
    3.23                ("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50)
    3.24  
    3.25 -  lconf    :: "'c prog => aheap => ('a \<leadsto> val) => ('a \<leadsto> ty) => bool"
    3.26 +  lconf    :: "'c prog => aheap => ('a \<rightharpoonup> val) => ('a \<rightharpoonup> ty) => bool"
    3.27                ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50)
    3.28  
    3.29    oconf    :: "'c prog => aheap => obj => bool"
     4.1 --- a/src/HOL/MicroJava/J/Decl.thy	Fri Jul 25 10:52:15 2003 +0200
     4.2 +++ b/src/HOL/MicroJava/J/Decl.thy	Fri Jul 25 17:21:22 2003 +0200
     4.3 @@ -33,7 +33,7 @@
     4.4  
     4.5  
     4.6  constdefs
     4.7 -  class :: "'c prog => (cname \<leadsto> 'c class)"
     4.8 +  class :: "'c prog => (cname \<rightharpoonup> 'c class)"
     4.9    "class \<equiv> map_of"
    4.10  
    4.11    is_class :: "'c prog => cname => bool"
     5.1 --- a/src/HOL/MicroJava/J/State.thy	Fri Jul 25 10:52:15 2003 +0200
     5.2 +++ b/src/HOL/MicroJava/J/State.thy	Fri Jul 25 17:21:22 2003 +0200
     5.3 @@ -9,7 +9,7 @@
     5.4  theory State = TypeRel + Value:
     5.5  
     5.6  types 
     5.7 -  fields_ = "(vname \<times> cname \<leadsto> val)"  -- "field name, defining class, value"
     5.8 +  fields_ = "(vname \<times> cname \<rightharpoonup> val)"  -- "field name, defining class, value"
     5.9  
    5.10    obj = "cname \<times> fields_"    -- "class instance with class name and fields"
    5.11  
    5.12 @@ -17,12 +17,12 @@
    5.13    obj_ty  :: "obj => ty"
    5.14   "obj_ty obj  == Class (fst obj)"
    5.15  
    5.16 -  init_vars :: "('a \<times> ty) list => ('a \<leadsto> val)"
    5.17 +  init_vars :: "('a \<times> ty) list => ('a \<rightharpoonup> val)"
    5.18   "init_vars == map_of o map (\<lambda>(n,T). (n,default_val T))"
    5.19    
    5.20  
    5.21 -types aheap  = "loc \<leadsto> obj"    -- {* "@{text heap}" used in a translation below *}
    5.22 -      locals = "vname \<leadsto> val"  -- "simple state, i.e. variable contents"
    5.23 +types aheap  = "loc \<rightharpoonup> obj"    -- {* "@{text heap}" used in a translation below *}
    5.24 +      locals = "vname \<rightharpoonup> val"  -- "simple state, i.e. variable contents"
    5.25  
    5.26        state  = "aheap \<times> locals"      -- "heap, local parameter including This"
    5.27        xstate = "val option \<times> state" -- "state including exception information"
     6.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Fri Jul 25 10:52:15 2003 +0200
     6.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Fri Jul 25 17:21:22 2003 +0200
     6.3 @@ -81,8 +81,8 @@
     6.4  
     6.5  consts
     6.6  
     6.7 -  method :: "'c prog \<times> cname => ( sig   \<leadsto> cname \<times> ty \<times> 'c)" (* ###curry *)
     6.8 -  field  :: "'c prog \<times> cname => ( vname \<leadsto> cname \<times> ty     )" (* ###curry *)
     6.9 +  method :: "'c prog \<times> cname => ( sig   \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
    6.10 +  field  :: "'c prog \<times> cname => ( vname \<rightharpoonup> cname \<times> ty     )" (* ###curry *)
    6.11    fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *)
    6.12  
    6.13  -- "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6"
     7.1 --- a/src/HOL/MicroJava/J/WellType.thy	Fri Jul 25 10:52:15 2003 +0200
     7.2 +++ b/src/HOL/MicroJava/J/WellType.thy	Fri Jul 25 17:21:22 2003 +0200
     7.3 @@ -24,12 +24,12 @@
     7.4  
     7.5  text "local variables, including method parameters and This:"
     7.6  types 
     7.7 -  lenv   = "vname \<leadsto> ty"
     7.8 +  lenv   = "vname \<rightharpoonup> ty"
     7.9    'c env = "'c prog \<times> lenv"
    7.10  
    7.11  syntax
    7.12    prg    :: "'c env => 'c prog"
    7.13 -  localT :: "'c env => (vname \<leadsto> ty)"
    7.14 +  localT :: "'c env => (vname \<rightharpoonup> ty)"
    7.15  
    7.16  translations  
    7.17    "prg"    => "fst"
     8.1 --- a/src/HOL/NanoJava/Decl.thy	Fri Jul 25 10:52:15 2003 +0200
     8.2 +++ b/src/HOL/NanoJava/Decl.thy	Fri Jul 25 17:21:22 2003 +0200
     8.3 @@ -52,7 +52,7 @@
     8.4  
     8.5  
     8.6  constdefs
     8.7 -  class	     :: "cname \<leadsto> class"
     8.8 +  class	     :: "cname \<rightharpoonup> class"
     8.9   "class      \<equiv> map_of Prog"
    8.10  
    8.11    is_class   :: "cname => bool"
     9.1 --- a/src/HOL/NanoJava/State.thy	Fri Jul 25 10:52:15 2003 +0200
     9.2 +++ b/src/HOL/NanoJava/State.thy	Fri Jul 25 17:21:22 2003 +0200
     9.3 @@ -21,7 +21,7 @@
     9.4    | Addr loc    --{* address, i.e. location of object *}
     9.5  
     9.6  types	fields
     9.7 -	= "(fname \<leadsto> val)"
     9.8 +	= "(fname \<rightharpoonup> val)"
     9.9  
    9.10          obj = "cname \<times> fields"
    9.11  
    9.12 @@ -32,12 +32,12 @@
    9.13  
    9.14  constdefs
    9.15  
    9.16 -  init_vars:: "('a \<leadsto> 'b) => ('a \<leadsto> val)"
    9.17 +  init_vars:: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> val)"
    9.18   "init_vars m == option_map (\<lambda>T. Null) o m"
    9.19    
    9.20  text {* private: *}
    9.21 -types	heap   = "loc   \<leadsto> obj"
    9.22 -        locals = "vname \<leadsto> val"	
    9.23 +types	heap   = "loc   \<rightharpoonup> obj"
    9.24 +        locals = "vname \<rightharpoonup> val"	
    9.25  
    9.26  text {* private: *}
    9.27  record  state
    10.1 --- a/src/HOL/NanoJava/TypeRel.thy	Fri Jul 25 10:52:15 2003 +0200
    10.2 +++ b/src/HOL/NanoJava/TypeRel.thy	Fri Jul 25 17:21:22 2003 +0200
    10.3 @@ -27,8 +27,8 @@
    10.4    "S \<preceq>   T" == "(S,T) \<in> widen"
    10.5  
    10.6  consts
    10.7 -  method :: "cname => (mname \<leadsto> methd)"
    10.8 -  field  :: "cname => (fname \<leadsto> ty)"
    10.9 +  method :: "cname => (mname \<rightharpoonup> methd)"
   10.10 +  field  :: "cname => (fname \<rightharpoonup> ty)"
   10.11  
   10.12  
   10.13  subsection "Declarations and properties not used in the meta theory"
   10.14 @@ -102,7 +102,7 @@
   10.15  by (auto intro: finite_acyclic_wf_converse finite_subcls1 subcls1_acyclic)
   10.16  
   10.17  
   10.18 -consts class_rec ::"cname \<Rightarrow> (class \<Rightarrow> ('a \<times> 'b) list) \<Rightarrow> ('a \<leadsto> 'b)"
   10.19 +consts class_rec ::"cname \<Rightarrow> (class \<Rightarrow> ('a \<times> 'b) list) \<Rightarrow> ('a \<rightharpoonup> 'b)"
   10.20  
   10.21  recdef (permissive) class_rec "subcls1\<inverse>"
   10.22        "class_rec C = (\<lambda>f. case class C of None   \<Rightarrow> arbitrary