# HG changeset patch # User nipkow # Date 1333436106 -7200 # Node ID 56d72c9232818ef63acb9c555cef83c8cd3a9a27 # Parent ce898681f700c2ee7b68349017a90b220ca88de1 made sure that " is shown in tutorial text diff -r ce898681f700 -r 56d72c923281 doc-src/ProgProve/Makefile --- a/doc-src/ProgProve/Makefile Mon Apr 02 21:26:46 2012 +0100 +++ b/doc-src/ProgProve/Makefile Tue Apr 03 08:55:06 2012 +0200 @@ -10,7 +10,7 @@ NAME = prog-prove FILES = prog-prove.tex prog-prove.bib Thys/document/*.tex prelude.tex \ - svmono.cls mathpartir.sty isabelle.sty isabellesym.sty + svmono.cls mathpartir.sty isabelle.sty isabellesym.sty Thys/MyList.thy dvi: $(NAME).dvi diff -r ce898681f700 -r 56d72c923281 doc-src/ProgProve/Thys/Bool_nat_list.thy --- a/doc-src/ProgProve/Thys/Bool_nat_list.thy Mon Apr 02 21:26:46 2012 +0100 +++ b/doc-src/ProgProve/Thys/Bool_nat_list.thy Tue Apr 03 08:55:06 2012 +0200 @@ -387,10 +387,11 @@ @{text"length :: 'a list \ nat"} (with the obvious definition), and the map function that applies a function to all elements of a list: \begin{isabelle} -\isacom{fun} @{text "map :: ('a \ 'b) \ 'a list \ 'b list"}\\ -@{thm map.simps(1)} @{text"|"}\\ -@{thm map.simps(2)} +\isacom{fun} @{const map} @{text"::"} @{typ[source] "('a \ 'b) \ 'a list \ 'b list"}\\ +@{text"\""}@{thm map.simps(1)}@{text"\" |"}\\ +@{text"\""}@{thm map.simps(2)}@{text"\""} \end{isabelle} +\sem Also useful are the \concept{head} of a list, its first element, and the \concept{tail}, the rest of the list: \begin{isabelle} @@ -405,6 +406,8 @@ Note that since HOL is a logic of total functions, @{term"hd []"} is defined, but we do now know what the result is. That is, @{term"hd []"} is not undefined but underdefined. +\endsem +% *} (*<*) end diff -r ce898681f700 -r 56d72c923281 doc-src/ProgProve/Thys/Isar.thy --- a/doc-src/ProgProve/Thys/Isar.thy Mon Apr 02 21:26:46 2012 +0100 +++ b/doc-src/ProgProve/Thys/Isar.thy Tue Apr 03 08:55:06 2012 +0200 @@ -178,7 +178,7 @@ \subsection{Structured lemma statements: \isacom{fixes}, \isacom{assumes}, \isacom{shows}} Lemmas can also be stated in a more structured fashion. To demonstrate this -feature with Cantor's theorem, we rephrase \noquotes{@{prop[source]"\ surj f"}} +feature with Cantor's theorem, we rephrase @{prop"\ surj f"} a little: *} @@ -190,7 +190,8 @@ txt{* The optional \isacom{fixes} part allows you to state the types of variables up front rather than by decorating one of their occurrences in the formula with a type constraint. The key advantage of the structured format is -the \isacom{assumes} part that allows you to name each assumption. The +the \isacom{assumes} part that allows you to name each assumption; multiple +assumptions can be separated by \isacom{and}. The \isacom{shows} part gives the goal. The actual theorem that will come out of the proof is @{prop"surj f \ False"}, but during the proof the assumption @{prop"surj f"} is available under the name @{text s} like any other fact. @@ -393,7 +394,8 @@ text_raw{* \begin{isamarkuptext}% -How to prove set equality and subset relationship: + +Finally, how to prove set equality and subset relationship: \end{isamarkuptext}% \begin{tabular}{@ {}ll@ {}} \begin{minipage}[t]{.4\textwidth} @@ -544,7 +546,7 @@ \subsection{Raw proof blocks} -Sometimes one would like to prove some lemma locally with in a proof. +Sometimes one would like to prove some lemma locally within a proof. A lemma that shares the current context of assumptions but that has its own assumptions and is generalised over its locally fixed variables at the end. This is what a \concept{raw proof block} does: @@ -745,7 +747,7 @@ \begin{quote} \isacom{fix} @{text n}\\ \isacom{assume} @{text"Suc:"} - \begin{tabular}[t]{l}@{text"A(n) \ P(n)"}\\@{text"A(Suc n)"}\end{tabular}\\ + \begin{tabular}[t]{l}@{text"\"A(n) \ P(n)\""}\\@{text"\"A(Suc n)\""}\end{tabular}\\ \isacom{let} @{text"?case = \"P(Suc n)\""} \end{quote} The list of assumptions @{text Suc} is actually subdivided @@ -812,8 +814,8 @@ ~\\ \isacom{fix} @{text n}\\ \isacom{assume} @{text"evSS:"} - \begin{tabular}[t]{l} @{text"ev n"}\\@{text"even n"}\end{tabular}\\ -\isacom{let} @{text"?case = even(Suc(Suc n))"}\\ + \begin{tabular}[t]{l} @{text"\"ev n\""}\\@{text"\"even n\""}\end{tabular}\\ +\isacom{let} @{text"?case = \"even(Suc(Suc n))\""}\\ \end{minipage} \end{tabular} \medskip diff -r ce898681f700 -r 56d72c923281 doc-src/ProgProve/Thys/Logic.thy --- a/doc-src/ProgProve/Thys/Logic.thy Mon Apr 02 21:26:46 2012 +0100 +++ b/doc-src/ProgProve/Thys/Logic.thy Tue Apr 03 08:55:06 2012 +0200 @@ -438,7 +438,7 @@ inductive ev :: "nat \ bool" where ev0: "ev 0" | evSS: (*<*)"ev n \ ev (Suc(Suc n))"(*>*) -text_raw{* @{prop"ev n \ ev (n + 2)"} *} +text_raw{* @{prop[source]"ev n \ ev (n + 2)"} *} text{* To get used to inductive definitions, we will first prove a few properties of @{const ev} informally before we descend to the Isabelle level. diff -r ce898681f700 -r 56d72c923281 doc-src/ProgProve/Thys/Types_and_funs.thy --- a/doc-src/ProgProve/Thys/Types_and_funs.thy Mon Apr 02 21:26:46 2012 +0100 +++ b/doc-src/ProgProve/Thys/Types_and_funs.thy Tue Apr 03 08:55:06 2012 +0200 @@ -55,7 +55,7 @@ As an example, consider binary trees: *} -datatype 'a tree = Tip | Node "('a tree)" 'a "('a tree)" +datatype 'a tree = Tip | Node "'a tree" 'a "'a tree" text{* with a mirror function: *} @@ -86,8 +86,8 @@ done (*>*) fun lookup :: "('a * 'b) list \ 'a \ 'b option" where -"lookup [] x' = None" | -"lookup ((x,y) # ps) x' = (if x = x' then Some y else lookup ps x')" +"lookup [] x = None" | +"lookup ((a,b) # ps) x = (if a = x then Some b else lookup ps x)" text{* Note that @{text"\\<^isub>1 * \\<^isub>2"} is the type of pairs, also written @{text"\\<^isub>1 \ \\<^isub>2"}. diff -r ce898681f700 -r 56d72c923281 doc-src/ProgProve/Thys/document/Bool_nat_list.tex --- a/doc-src/ProgProve/Thys/document/Bool_nat_list.tex Mon Apr 02 21:26:46 2012 +0100 +++ b/doc-src/ProgProve/Thys/document/Bool_nat_list.tex Tue Apr 03 08:55:06 2012 +0200 @@ -557,10 +557,11 @@ \isa{length\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat} (with the obvious definition), and the map function that applies a function to all elements of a list: \begin{isabelle} -\isacom{fun} \isa{map\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ list}\\ -\isa{map\ f\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} \isa{{\isaliteral{7C}{\isacharbar}}}\\ -\isa{map\ f\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ x\ {\isaliteral{23}{\isacharhash}}\ map\ f\ xs} +\isacom{fun} \isa{map} \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}} \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ list{\isaliteral{22}{\isachardoublequote}}}\\ +\isa{{\isaliteral{22}{\isachardoublequote}}}\isa{map\ f\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}\isa{{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{7C}{\isacharbar}}}\\ +\isa{{\isaliteral{22}{\isachardoublequote}}}\isa{map\ f\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ x\ {\isaliteral{23}{\isacharhash}}\ map\ f\ xs}\isa{{\isaliteral{22}{\isachardoublequote}}} \end{isabelle} +\sem Also useful are the \concept{head} of a list, its first element, and the \concept{tail}, the rest of the list: \begin{isabelle} @@ -574,7 +575,9 @@ \end{isabelle} Note that since HOL is a logic of total functions, \isa{hd\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} is defined, but we do now know what the result is. That is, \isa{hd\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} is not undefined -but underdefined.% +but underdefined. +\endsem +%% \end{isamarkuptext}% \isamarkuptrue% % diff -r ce898681f700 -r 56d72c923281 doc-src/ProgProve/Thys/document/Isar.tex --- a/doc-src/ProgProve/Thys/document/Isar.tex Mon Apr 02 21:26:46 2012 +0100 +++ b/doc-src/ProgProve/Thys/document/Isar.tex Tue Apr 03 08:55:06 2012 +0200 @@ -269,7 +269,7 @@ \subsection{Structured lemma statements: \isacom{fixes}, \isacom{assumes}, \isacom{shows}} Lemmas can also be stated in a more structured fashion. To demonstrate this -feature with Cantor's theorem, we rephrase \noquotes{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ surj\ f{\isaliteral{22}{\isachardoublequote}}}} +feature with Cantor's theorem, we rephrase \isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ surj\ f} a little:% \end{isamarkuptext}% \isamarkuptrue% @@ -288,7 +288,8 @@ The optional \isacom{fixes} part allows you to state the types of variables up front rather than by decorating one of their occurrences in the formula with a type constraint. The key advantage of the structured format is -the \isacom{assumes} part that allows you to name each assumption. The +the \isacom{assumes} part that allows you to name each assumption; multiple +assumptions can be separated by \isacom{and}. The \isacom{shows} part gives the goal. The actual theorem that will come out of the proof is \isa{surj\ f\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ False}, but during the proof the assumption \isa{surj\ f} is available under the name \isa{s} like any other fact.% @@ -672,7 +673,8 @@ \endisadelimproof % \begin{isamarkuptext}% -How to prove set equality and subset relationship: + +Finally, how to prove set equality and subset relationship: \end{isamarkuptext}% \begin{tabular}{@ {}ll@ {}} \begin{minipage}[t]{.4\textwidth} @@ -942,7 +944,7 @@ \subsection{Raw proof blocks} -Sometimes one would like to prove some lemma locally with in a proof. +Sometimes one would like to prove some lemma locally within a proof. A lemma that shares the current context of assumptions but that has its own assumptions and is generalised over its locally fixed variables at the end. This is what a \concept{raw proof block} does: @@ -1307,7 +1309,7 @@ \begin{quote} \isacom{fix} \isa{n}\\ \isacom{assume} \isa{Suc{\isaliteral{3A}{\isacharcolon}}} - \begin{tabular}[t]{l}\isa{A{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}}\\\isa{A{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}}\end{tabular}\\ + \begin{tabular}[t]{l}\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\end{tabular}\\ \isacom{let} \isa{{\isaliteral{3F}{\isacharquery}}case\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}P{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \end{quote} The list of assumptions \isa{Suc} is actually subdivided @@ -1399,8 +1401,8 @@ ~\\ \isacom{fix} \isa{n}\\ \isacom{assume} \isa{evSS{\isaliteral{3A}{\isacharcolon}}} - \begin{tabular}[t]{l} \isa{ev\ n}\\\isa{even\ n}\end{tabular}\\ -\isacom{let} \isa{{\isaliteral{3F}{\isacharquery}}case\ {\isaliteral{3D}{\isacharequal}}\ even{\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}\\ + \begin{tabular}[t]{l} \isa{{\isaliteral{22}{\isachardoublequote}}ev\ n{\isaliteral{22}{\isachardoublequote}}}\\\isa{{\isaliteral{22}{\isachardoublequote}}even\ n{\isaliteral{22}{\isachardoublequote}}}\end{tabular}\\ +\isacom{let} \isa{{\isaliteral{3F}{\isacharquery}}case\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}even{\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\ \end{minipage} \end{tabular} \medskip diff -r ce898681f700 -r 56d72c923281 doc-src/ProgProve/Thys/document/Logic.tex --- a/doc-src/ProgProve/Thys/document/Logic.tex Mon Apr 02 21:26:46 2012 +0100 +++ b/doc-src/ProgProve/Thys/document/Logic.tex Tue Apr 03 08:55:06 2012 +0200 @@ -570,7 +570,7 @@ \ ev\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline ev{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}\ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}ev\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline evSS{\isaliteral{3A}{\isacharcolon}}\ \ % -\isa{ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ev\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} +\isa{{\isaliteral{22}{\isachardoublequote}}ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ev\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} % \begin{isamarkuptext}% To get used to inductive definitions, we will first prove a few diff -r ce898681f700 -r 56d72c923281 doc-src/ProgProve/Thys/document/Types_and_funs.tex --- a/doc-src/ProgProve/Thys/document/Types_and_funs.tex Mon Apr 02 21:26:46 2012 +0100 +++ b/doc-src/ProgProve/Thys/document/Types_and_funs.tex Tue Apr 03 08:55:06 2012 +0200 @@ -68,7 +68,7 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{datatype}\isamarkupfalse% -\ {\isaliteral{27}{\isacharprime}}a\ tree\ {\isaliteral{3D}{\isacharequal}}\ Tip\ {\isaliteral{7C}{\isacharbar}}\ Node\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ tree{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ tree{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% +\ {\isaliteral{27}{\isacharprime}}a\ tree\ {\isaliteral{3D}{\isacharequal}}\ Tip\ {\isaliteral{7C}{\isacharbar}}\ Node\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ tree{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{27}{\isacharprime}}a\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ tree{\isaliteral{22}{\isachardoublequoteclose}}% \begin{isamarkuptext}% with a mirror function:% \end{isamarkuptext}% @@ -122,8 +122,8 @@ \endisadelimproof \isacommand{fun}\isamarkupfalse% \ lookup\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline -{\isaliteral{22}{\isachardoublequoteopen}}lookup\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ x{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ None{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline -{\isaliteral{22}{\isachardoublequoteopen}}lookup\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{23}{\isacharhash}}\ ps{\isaliteral{29}{\isacharparenright}}\ x{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ x\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{27}{\isacharprime}}\ then\ Some\ y\ else\ lookup\ ps\ x{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% +{\isaliteral{22}{\isachardoublequoteopen}}lookup\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ x\ {\isaliteral{3D}{\isacharequal}}\ None{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline +{\isaliteral{22}{\isachardoublequoteopen}}lookup\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{23}{\isacharhash}}\ ps{\isaliteral{29}{\isacharparenright}}\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ a\ {\isaliteral{3D}{\isacharequal}}\ x\ then\ Some\ b\ else\ lookup\ ps\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% \begin{isamarkuptext}% Note that \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}} is the type of pairs, also written \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}.