# HG changeset patch
# User haftmann
# Date 1159196659 -7200
# Node ID 8b79d853eabb7472fd24f69ee15ba5969df0f19f
# Parent  17a625996bb091e6d0ee961be1131b9716c87ad2
added examples for variable name handling

diff -r 17a625996bb0 -r 8b79d853eabb src/HOL/ex/Codegenerator.thy
--- a/src/HOL/ex/Codegenerator.thy	Mon Sep 25 17:04:18 2006 +0200
+++ b/src/HOL/ex/Codegenerator.thy	Mon Sep 25 17:04:19 2006 +0200
@@ -73,6 +73,11 @@
 
 subsection {* equalities *}
 
+subsection {* strings *}
+
+definition
+  "mystring = ''my home is my castle''"
+
 subsection {* heavy usage of names *}
 
 definition
@@ -88,16 +93,28 @@
   g "Mymod.A.f"
   h "Mymod.A.B.f"
 
+definition
+  "apply_tower = (\<lambda>x. x (\<lambda>x. x (\<lambda>x. x)))"
+
+definition
+  "keywords fun datatype class instance funa classa =
+    Suc fun + datatype * class mod instance - funa - classa"
+
+hide (open) const keywords
+
+definition
+  "shadow keywords = keywords @ [Codegenerator.keywords 0 0 0 0 0 0]"
+
 code_gen xor
 code_gen one
+code_gen
+  Pair fst snd Let split swap
 code_gen "0::int" "1::int"
   (SML) (Haskell)
 code_gen n
   (SML) (Haskell)
 code_gen fac
   (SML) (Haskell)
-code_gen n
-  (SML) (Haskell)
 code_gen
   "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
   "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
@@ -105,8 +122,6 @@
   "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"
   "op <= :: nat \<Rightarrow> nat \<Rightarrow> bool"
 code_gen
-  Pair fst snd Let split swap
-code_gen
   appl
 code_gen
   k
@@ -151,8 +166,12 @@
   "OperationalEquality.eq :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
   "OperationalEquality.eq :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
 code_gen
+  mystring
+code_gen
   f g h
+code_gen
+  apply_tower Codegenerator.keywords shadow
 
-code_gen (SML -) (SML _)
+code_gen (SML -)
 
 end
\ No newline at end of file