--- 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";
--- 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
--- 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
--- 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
--- 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
--- 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*}
--- 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}}%