doc-src/TutorialI/Misc/pairs.thy

renamed // to / (which is what we want anyway) to avoid clash with the new
use of // for quotienting

(*<*)
theory pairs = Main:;
term(*>*) "let (x,y) = f z in (y,x)";
(*<*)
term(*>*) "case xs of [] \\<Rightarrow> 0 | (x,y)#zs \\<Rightarrow> x+y"
(**)(*<*)
end
(*>*)