--- a/etc/isar-keywords-ZF.el Mon Jan 23 14:06:40 2006 +0100
+++ b/etc/isar-keywords-ZF.el Mon Jan 23 14:07:52 2006 +0100
@@ -202,14 +202,12 @@
'("advanced"
"and"
"assumes"
- "atom"
"attach"
"begin"
"binder"
"case_eqns"
"con_defs"
"concl"
- "constants"
"constrains"
"contains"
"defines"
@@ -236,6 +234,7 @@
"recursor_eqns"
"shows"
"structure"
+ "target_atom"
"type_elims"
"type_intros"
"uses"
--- a/etc/isar-keywords.el Mon Jan 23 14:06:40 2006 +0100
+++ b/etc/isar-keywords.el Mon Jan 23 14:07:52 2006 +0100
@@ -217,14 +217,12 @@
"advanced"
"and"
"assumes"
- "atom"
"attach"
"begin"
"binder"
"compose"
"concl"
"congs"
- "constants"
"constrains"
"contains"
"defines"
@@ -265,6 +263,7 @@
"signature"
"states"
"structure"
+ "target_atom"
"to"
"transitions"
"transrel"
--- a/src/HOL/Datatype.thy Mon Jan 23 14:06:40 2006 +0100
+++ b/src/HOL/Datatype.thy Mon Jan 23 14:07:52 2006 +0100
@@ -224,16 +224,16 @@
code_syntax_const
True
- ml (atom "true")
- haskell (atom "True")
+ ml (target_atom "true")
+ haskell (target_atom "True")
False
- ml (atom "false")
- haskell (atom "False")
+ ml (target_atom "false")
+ haskell (target_atom "False")
code_syntax_const
Pair
- ml (atom "(__,/ __)")
- haskell (atom "(__,/ __)")
+ ml (target_atom "(__,/ __)")
+ haskell (target_atom "(__,/ __)")
code_syntax_const
1 :: "nat"
--- a/src/HOL/HOL.thy Mon Jan 23 14:06:40 2006 +0100
+++ b/src/HOL/HOL.thy Mon Jan 23 14:07:52 2006 +0100
@@ -1377,13 +1377,13 @@
uminus "HOL.uminus"
code_syntax_tyco bool
- ml (atom "bool")
- haskell (atom "Bool")
+ ml (target_atom "bool")
+ haskell (target_atom "Bool")
code_syntax_const
Not
- ml (atom "not")
- haskell (atom "not")
+ ml (target_atom "not")
+ haskell (target_atom "not")
"op &"
ml (infixl 1 "andalso")
haskell (infixl 3 "&&")
--- a/src/HOL/Integ/IntDef.thy Mon Jan 23 14:06:40 2006 +0100
+++ b/src/HOL/Integ/IntDef.thy Mon Jan 23 14:07:52 2006 +0100
@@ -897,16 +897,16 @@
"neg" ("(_ < 0)")
code_syntax_tyco int
- ml (atom "IntInf.int")
- haskell (atom "Integer")
+ ml (target_atom "IntInf.int")
+ haskell (target_atom "Integer")
code_syntax_const
0 :: "int"
- ml (atom "(0:IntInf.int)")
- haskell (atom "0")
+ ml (target_atom "(0:IntInf.int)")
+ haskell (target_atom "0")
1 :: "int"
- ml (atom "(1:IntInf.int)")
- haskell (atom "1")
+ ml (target_atom "(1:IntInf.int)")
+ haskell (target_atom "1")
"op +" :: "int \<Rightarrow> int \<Rightarrow> int"
ml (infixl 8 "+")
haskell (infixl 6 "+")
@@ -914,8 +914,8 @@
ml (infixl 9 "*")
haskell (infixl 7 "*")
uminus :: "int \<Rightarrow> int"
- ml (atom "~")
- haskell (atom "negate")
+ ml (target_atom "~")
+ haskell (target_atom "negate")
"op <" :: "int \<Rightarrow> int \<Rightarrow> bool"
ml (infix 6 "<")
haskell (infix 4 "<")
--- a/src/HOL/Library/EfficientNat.thy Mon Jan 23 14:06:40 2006 +0100
+++ b/src/HOL/Library/EfficientNat.thy Mon Jan 23 14:07:52 2006 +0100
@@ -52,12 +52,12 @@
int ("(_)")
(* code_syntax_tyco nat
- ml (atom "InfInt.int")
- haskell (atom "Integer")
+ ml (target_atom "InfInt.int")
+ haskell (target_atom "Integer")
code_syntax_const 0 :: nat
ml ("0 : InfInt.int")
- haskell (atom "0")
+ haskell (target_atom "0")
code_syntax_const Suc
ml (infixl 8 "_ + 1")
--- a/src/HOL/Library/ExecutableSet.thy Mon Jan 23 14:06:40 2006 +0100
+++ b/src/HOL/Library/ExecutableSet.thy Mon Jan 23 14:07:52 2006 +0100
@@ -29,11 +29,11 @@
code_syntax_tyco set
ml ("_ list")
- haskell (atom "[_]")
+ haskell (target_atom "[_]")
code_syntax_const "{}"
- ml (atom "[]")
- haskell (atom "[]")
+ ml (target_atom "[]")
+ haskell (target_atom "[]")
consts_code
"{}" ("[]")
--- a/src/HOL/List.thy Mon Jan 23 14:06:40 2006 +0100
+++ b/src/HOL/List.thy Mon Jan 23 14:07:52 2006 +0100
@@ -2694,12 +2694,12 @@
code_syntax_tyco
list
ml ("_ list")
- haskell (atom "[_]")
+ haskell (target_atom "[_]")
code_syntax_const
Nil
- ml (atom "[]")
- haskell (atom "[]")
+ ml (target_atom "[]")
+ haskell (target_atom "[]")
setup list_codegen_setup
--- a/src/HOL/Product_Type.thy Mon Jan 23 14:06:40 2006 +0100
+++ b/src/HOL/Product_Type.thy Mon Jan 23 14:07:52 2006 +0100
@@ -798,13 +798,13 @@
code_syntax_tyco
*
ml (infix 2 "*")
- haskell (atom "(__,/ __)")
+ haskell (target_atom "(__,/ __)")
code_syntax_const
fst
- haskell (atom "fst")
+ haskell (target_atom "fst")
snd
- haskell (atom "snd")
+ haskell (target_atom "snd")
ML {*