Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/MicroJava/JVM/Store.thy
changeset 8034 6fc37b5c5e98
parent 8011 d14c4e9e9c8e
child 8038 a13c3b80d3d4 
--- a/src/HOL/MicroJava/JVM/Store.thy	Thu Nov 25 12:30:57 1999 +0100
+++ b/src/HOL/MicroJava/JVM/Store.thy	Fri Nov 26 08:46:59 1999 +0100
@@ -12,9 +12,9 @@
 Store = Conform +  
 
 syntax
- value	:: "['a \\<leadsto> 'b,'a] \\<Rightarrow> 'b"			("_ \\<And> _")		
+ map_apply :: "['a \\<leadsto> 'b,'a] \\<Rightarrow> 'b"	("_ !! _")
 translations
- "t \\<And> x"  == "the (t x)"
+ "t !! x"  == "the (t x)"
 
 constdefs
  newref :: "('a \\<leadsto> 'b) \\<Rightarrow> 'a"
isabelle