# HG changeset patch
# User wenzelm
# Date 1305213477 -7200
# Node ID aec61b60ff7bcf5bb8758df6e67dcecd9f8a9f6b
# Parent  ab07cb4513903df9949656db96127215a7ae39c6
modernized specifications;

diff -r ab07cb451390 -r aec61b60ff7b doc-src/TutorialI/CodeGen/CodeGen.thy
--- a/doc-src/TutorialI/CodeGen/CodeGen.thy	Thu May 12 16:58:55 2011 +0200
+++ b/doc-src/TutorialI/CodeGen/CodeGen.thy	Thu May 12 17:17:57 2011 +0200
@@ -15,7 +15,7 @@
 appropriate function itself.
 *}
 
-types 'v binop = "'v \<Rightarrow> 'v \<Rightarrow> 'v";
+type_synonym 'v binop = "'v \<Rightarrow> 'v \<Rightarrow> 'v";
 datatype ('a,'v)expr = Cex 'v
                      | Vex 'a
                      | Bex "'v binop"  "('a,'v)expr"  "('a,'v)expr";
diff -r ab07cb451390 -r aec61b60ff7b doc-src/TutorialI/CodeGen/document/CodeGen.tex
--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Thu May 12 16:58:55 2011 +0200
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Thu May 12 17:17:57 2011 +0200
@@ -31,7 +31,7 @@
 appropriate function itself.%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{types}\isamarkupfalse%
+\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}\isamarkupfalse%
 \ {\isaliteral{27}{\isacharprime}}v\ binop\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}v\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}v\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}v{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \isacommand{datatype}\isamarkupfalse%
 \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{29}{\isacharparenright}}expr\ {\isaliteral{3D}{\isacharequal}}\ Cex\ {\isaliteral{27}{\isacharprime}}v\isanewline
diff -r ab07cb451390 -r aec61b60ff7b doc-src/TutorialI/Misc/document/types.tex
--- a/doc-src/TutorialI/Misc/document/types.tex	Thu May 12 16:58:55 2011 +0200
+++ b/doc-src/TutorialI/Misc/document/types.tex	Thu May 12 17:17:57 2011 +0200
@@ -14,10 +14,12 @@
 \isadelimtheory
 %
 \endisadelimtheory
-\isacommand{types}\isamarkupfalse%
-\ number\ \ \ \ \ \ \ {\isaliteral{3D}{\isacharequal}}\ nat\isanewline
-\ \ \ \ \ \ gate\ \ \ \ \ \ \ \ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}alist\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}list{\isaliteral{22}{\isachardoublequoteclose}}%
+\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}\isamarkupfalse%
+\ number\ {\isaliteral{3D}{\isacharequal}}\ nat\isanewline
+\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}\isamarkupfalse%
+\ gate\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ alist\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ list{\isaliteral{22}{\isachardoublequoteclose}}%
 \begin{isamarkuptext}%
 \noindent
 Internally all synonyms are fully expanded.  As a consequence Isabelle's
diff -r ab07cb451390 -r aec61b60ff7b doc-src/TutorialI/Misc/types.thy
--- a/doc-src/TutorialI/Misc/types.thy	Thu May 12 16:58:55 2011 +0200
+++ b/doc-src/TutorialI/Misc/types.thy	Thu May 12 17:17:57 2011 +0200
@@ -1,7 +1,7 @@
 (*<*)theory "types" imports Main begin(*>*)
-types number       = nat
-      gate         = "bool \<Rightarrow> bool \<Rightarrow> bool"
-      ('a,'b)alist = "('a \<times> 'b)list"
+type_synonym number = nat
+type_synonym gate = "bool \<Rightarrow> bool \<Rightarrow> bool"
+type_synonym ('a, 'b) alist = "('a \<times> 'b) list"
 
 text{*\noindent
 Internally all synonyms are fully expanded.  As a consequence Isabelle's
diff -r ab07cb451390 -r aec61b60ff7b doc-src/TutorialI/Overview/LNCS/FP1.thy
--- a/doc-src/TutorialI/Overview/LNCS/FP1.thy	Thu May 12 16:58:55 2011 +0200
+++ b/doc-src/TutorialI/Overview/LNCS/FP1.thy	Thu May 12 17:17:57 2011 +0200
@@ -148,7 +148,7 @@
 
 subsubsection{*Expressions*}
 
-types 'v binop = "'v \<Rightarrow> 'v \<Rightarrow> 'v"
+type_synonym 'v binop = "'v \<Rightarrow> 'v \<Rightarrow> 'v"
 
 datatype ('a,'v)expr = Cex 'v
                      | Vex 'a
diff -r ab07cb451390 -r aec61b60ff7b doc-src/TutorialI/Protocol/Message.thy
--- a/doc-src/TutorialI/Protocol/Message.thy	Thu May 12 16:58:55 2011 +0200
+++ b/doc-src/TutorialI/Protocol/Message.thy	Thu May 12 17:17:57 2011 +0200
@@ -32,7 +32,7 @@
 the matching private key, and vice versa:
 *}
 
-types key = nat
+type_synonym key = nat
 consts invKey :: "key \<Rightarrow> key"
 (*<*)
 consts all_symmetric :: bool        --{*true if all keys are symmetric*}
diff -r ab07cb451390 -r aec61b60ff7b doc-src/TutorialI/Protocol/document/Message.tex
--- a/doc-src/TutorialI/Protocol/document/Message.tex	Thu May 12 16:58:55 2011 +0200
+++ b/doc-src/TutorialI/Protocol/document/Message.tex	Thu May 12 17:17:57 2011 +0200
@@ -47,7 +47,7 @@
 the matching private key, and vice versa:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{types}\isamarkupfalse%
+\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}\isamarkupfalse%
 \ key\ {\isaliteral{3D}{\isacharequal}}\ nat\isanewline
 \isacommand{consts}\isamarkupfalse%
 \ invKey\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}key\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ key{\isaliteral{22}{\isachardoublequoteclose}}%