# HG changeset patch
# User wenzelm
# Date 1266099897 -3600
# Node ID e286d5df187a6631533201a9404260467ef43875
# Parent  305b3eb5b9d5bb8917c96445ca82de47153e4c28
modernized structures;

diff -r 305b3eb5b9d5 -r e286d5df187a src/HOL/Int.thy
--- 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"
diff -r 305b3eb5b9d5 -r e286d5df187a src/HOL/RealPow.thy
--- 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)"
diff -r 305b3eb5b9d5 -r e286d5df187a src/HOL/String.thy
--- 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,
diff -r 305b3eb5b9d5 -r e286d5df187a src/HOL/Tools/float_syntax.ML
--- 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 *)
diff -r 305b3eb5b9d5 -r e286d5df187a src/HOL/Tools/numeral_syntax.ML
--- 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 *)
diff -r 305b3eb5b9d5 -r e286d5df187a src/HOL/Tools/string_syntax.ML
--- 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))
diff -r 305b3eb5b9d5 -r e286d5df187a src/ZF/Bin.thy
--- 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]
diff -r 305b3eb5b9d5 -r e286d5df187a src/ZF/Tools/numeral_syntax.ML
--- 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 *)
diff -r 305b3eb5b9d5 -r e286d5df187a src/ZF/int_arith.ML
--- 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*)