--- a/src/HOL/Int.thy Sat Feb 13 23:16:06 2010 +0100
+++ b/src/HOL/Int.thy Sat Feb 13 23:24:57 2010 +0100
@@ -604,7 +604,7 @@
"_Numeral" :: "num_const \<Rightarrow> 'a" ("_")
use "Tools/numeral_syntax.ML"
-setup NumeralSyntax.setup
+setup Numeral_Syntax.setup
abbreviation
"Numeral0 \<equiv> number_of Pls"
--- a/src/HOL/RealPow.thy Sat Feb 13 23:16:06 2010 +0100
+++ b/src/HOL/RealPow.thy Sat Feb 13 23:24:57 2010 +0100
@@ -186,7 +186,7 @@
syntax "_Float" :: "float_const \<Rightarrow> 'a" ("_")
use "Tools/float_syntax.ML"
-setup FloatSyntax.setup
+setup Float_Syntax.setup
text{* Test: *}
lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::real)"
--- a/src/HOL/String.thy Sat Feb 13 23:16:06 2010 +0100
+++ b/src/HOL/String.thy Sat Feb 13 23:24:57 2010 +0100
@@ -79,7 +79,7 @@
"_String" :: "xstr => string" ("_")
use "Tools/string_syntax.ML"
-setup StringSyntax.setup
+setup String_Syntax.setup
definition chars :: string where
"chars = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
--- a/src/HOL/Tools/float_syntax.ML Sat Feb 13 23:16:06 2010 +0100
+++ b/src/HOL/Tools/float_syntax.ML Sat Feb 13 23:24:57 2010 +0100
@@ -8,7 +8,7 @@
val setup: theory -> theory
end;
-structure FloatSyntax: FLOAT_SYNTAX =
+structure Float_Syntax: FLOAT_SYNTAX =
struct
(* parse translation *)
--- a/src/HOL/Tools/numeral_syntax.ML Sat Feb 13 23:16:06 2010 +0100
+++ b/src/HOL/Tools/numeral_syntax.ML Sat Feb 13 23:24:57 2010 +0100
@@ -9,7 +9,7 @@
val setup: theory -> theory
end;
-structure NumeralSyntax: NUMERAL_SYNTAX =
+structure Numeral_Syntax: NUMERAL_SYNTAX =
struct
(* parse translation *)
--- a/src/HOL/Tools/string_syntax.ML Sat Feb 13 23:16:06 2010 +0100
+++ b/src/HOL/Tools/string_syntax.ML Sat Feb 13 23:24:57 2010 +0100
@@ -9,7 +9,7 @@
val setup: theory -> theory
end;
-structure StringSyntax: STRING_SYNTAX =
+structure String_Syntax: STRING_SYNTAX =
struct
@@ -19,7 +19,7 @@
val mk_nib =
Syntax.Constant o unprefix nib_prefix o
- fst o Term.dest_Const o HOLogic.mk_nibble;
+ fst o Term.dest_Const o HOLogic.mk_nibble;
fun dest_nib (Syntax.Constant c) =
HOLogic.dest_nibble (Const (nib_prefix ^ c, dummyT))
--- a/src/ZF/Bin.thy Sat Feb 13 23:16:06 2010 +0100
+++ b/src/ZF/Bin.thy Sat Feb 13 23:24:57 2010 +0100
@@ -105,7 +105,7 @@
"_Int" :: "xnum => i" ("_")
use "Tools/numeral_syntax.ML"
-setup NumeralSyntax.setup
+setup Numeral_Syntax.setup
declare bin.intros [simp,TC]
--- a/src/ZF/Tools/numeral_syntax.ML Sat Feb 13 23:16:06 2010 +0100
+++ b/src/ZF/Tools/numeral_syntax.ML Sat Feb 13 23:24:57 2010 +0100
@@ -14,7 +14,7 @@
val setup: theory -> theory
end;
-structure NumeralSyntax: NUMERAL_SYNTAX =
+structure Numeral_Syntax: NUMERAL_SYNTAX =
struct
(* bits *)
--- a/src/ZF/int_arith.ML Sat Feb 13 23:16:06 2010 +0100
+++ b/src/ZF/int_arith.ML Sat Feb 13 23:24:57 2010 +0100
@@ -22,7 +22,7 @@
fun term_of [] = @{term Pls}
| term_of [~1] = @{term Min}
| term_of (b :: bs) = @{term Bit} $ term_of bs $ mk_bit b;
- in term_of (NumeralSyntax.make_binary i) end;
+ in term_of (Numeral_Syntax.make_binary i) end;
fun dest_bin tm =
let
@@ -30,7 +30,7 @@
| bin_of @{term Min} = [~1]
| bin_of (@{term Bit} $ bs $ b) = dest_bit b :: bin_of bs
| bin_of _ = sys_error "dest_bin";
- in NumeralSyntax.dest_binary (bin_of tm) end;
+ in Numeral_Syntax.dest_binary (bin_of tm) end;
(*Utilities*)