equal
deleted
inserted
replaced
47 \attrdx{recdef_simp} attribute says to use \isa{less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le} as a |
47 \attrdx{recdef_simp} attribute says to use \isa{less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le} as a |
48 simplification rule.\cmmdx{hints}% |
48 simplification rule.\cmmdx{hints}% |
49 \end{isamarkuptext}% |
49 \end{isamarkuptext}% |
50 \isamarkuptrue% |
50 \isamarkuptrue% |
51 \isamarkupfalse% |
51 \isamarkupfalse% |
52 \isanewline |
|
53 \isamarkupfalse% |
52 \isamarkupfalse% |
54 \isacommand{recdef}\ qs\ {\isachardoublequote}measure\ length{\isachardoublequote}\isanewline |
53 \isacommand{recdef}\ qs\ {\isachardoublequote}measure\ length{\isachardoublequote}\isanewline |
55 \ {\isachardoublequote}qs\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline |
54 \ {\isachardoublequote}qs\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline |
56 \ {\isachardoublequote}qs{\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ y{\isasymle}x{\isacharparenright}\ xs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharat}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ x{\isacharless}y{\isacharparenright}\ xs{\isacharparenright}{\isachardoublequote}\isanewline |
55 \ {\isachardoublequote}qs{\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ y{\isasymle}x{\isacharparenright}\ xs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharat}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ x{\isacharless}y{\isacharparenright}\ xs{\isacharparenright}{\isachardoublequote}\isanewline |
57 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le{\isacharparenright}\isamarkupfalse% |
56 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le{\isacharparenright}\isanewline |
|
57 \isamarkupfalse% |
58 \isamarkupfalse% |
58 \isamarkupfalse% |
59 % |
59 % |
60 \begin{isamarkuptext}% |
60 \begin{isamarkuptext}% |
61 \noindent |
61 \noindent |
62 This time everything works fine. Now \isa{qs{\isachardot}simps} contains precisely |
62 This time everything works fine. Now \isa{qs{\isachardot}simps} contains precisely |
79 turn it permanently into a simplification rule, in which case the above |
79 turn it permanently into a simplification rule, in which case the above |
80 \isacommand{hint} is not necessary. But in the case of |
80 \isacommand{hint} is not necessary. But in the case of |
81 \isa{less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le} this would be of dubious value.% |
81 \isa{less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le} this would be of dubious value.% |
82 \end{isamarkuptext}% |
82 \end{isamarkuptext}% |
83 \isamarkuptrue% |
83 \isamarkuptrue% |
84 \isanewline |
|
85 \isamarkupfalse% |
84 \isamarkupfalse% |
86 \end{isabellebody}% |
85 \end{isabellebody}% |
87 %%% Local Variables: |
86 %%% Local Variables: |
88 %%% mode: latex |
87 %%% mode: latex |
89 %%% TeX-master: "root" |
88 %%% TeX-master: "root" |