adding temporary options to the quickcheck examples
% iman.sty : Isabelle Manual Page Layout%\typeout{Document Style iman. Released 17 February 1994}\hyphenation{Isa-belle man-u-script man-u-scripts ap-pen-dix mut-u-al-ly}\hyphenation{data-type data-types co-data-type co-data-types }\let\ts=\thinspace%usage: \iflabelundefined{LABEL}{if not defined}{if defined}\newcommand{\iflabelundefined}[1]{\@ifundefined{r@#1}}%%%INDEXING use sedindex to process the index\newcommand\seealso[2]{\emph{see also} #1}\usepackage{makeidx}%index, putting page numbers of definitions in boldface\def\bold#1{\textbf{#1}}\newcommand\fnote[1]{#1n}\newcommand\indexbold[1]{\index{#1|bold}}%for indexing constants, symbols, theorems, ...\newcommand\cdx[1]{{\tt#1}\index{#1@{\tt#1} constant}}\newcommand\sdx[1]{{\tt#1}\index{#1@{\tt#1} symbol}}\newcommand\tdx[1]{{\tt#1}\index{#1@{\tt#1} theorem}}\newcommand\tdxbold[1]{{\tt#1}\index{#1@{\tt#1} theorem|bold}}\newcommand\mltydx[1]{{\tt#1}\index{#1@{\tt#1} ML type}}\newcommand\xdx[1]{{\tt#1}\index{#1@{\tt#1} exception}}\newcommand\ndx[1]{{\tt#1}\index{#1@{\tt#1} nonterminal}}\newcommand\ndxbold[1]{{\tt#1}\index{#1@{\tt#1} nonterminal|bold}}\newcommand\cldx[1]{{\tt#1}\index{#1@{\tt#1} class}}\newcommand\tydx[1]{\textit{#1}\index{#1@{\textit{#1}} type}}\newcommand\thydx[1]{{\tt#1}\index{#1@{\tt#1} theory}}\newcommand\tooldx[1]{{\tt#1}\index{#1@{\tt#1} tool}}\newcommand\settdx[1]{{\tt#1}\index{#1@{\tt#1} setting}}%set argument in \tt font; at the same time, index using * prefix\newcommand\rmindex[1]{{#1}\index{#1}\@}\newcommand\ttindex[1]{{\tt#1}\index{*#1}\@}\newcommand\ttindexbold[1]{{\tt#1}\index{*#1|bold}\@}%set argument in \bf font and index in ROMAN font (for definitions in text!)\newcommand\bfindex[1]{{\bf#1}\index{#1|bold}\@}%%% underscores as ordinary characters, not for subscripting%% use @ or \sb for subscripting; use \at for @%% only works in \tt font%% must not make _ an active char; would make \ttindex fail!\gdef\underscoreoff{\catcode`\@=8\catcode`\_=\other}\gdef\underscoreon{\catcode`\_=8\makeatother}\chardef\other=12\chardef\at=`\@% alternative underscore\def\_{\leavevmode\kern.06em\vbox{\hrule height.2ex width.3em}\hskip0.1em}%%% \dquotes permits usage of "..." for \hbox{...} -- also taken from under.sty{\catcode`\"=\active\gdef\dquotes{\catcode`\"=\active \let"=\@mathText}%\gdef\@mathText#1"{\hbox{\mathTextFont #1\/}}}\def\mathTextFont{\frenchspacing\tt}\def\dquotesoff{\catcode`\"=\other}%%%% meta-logical connectives\let\Forall=\bigwedge\let\Imp=\Longrightarrow\let\To=\Rightarrow\newcommand{\PROP}{\mathop{\mathrm{PROP}}}\newcommand{\Var}[1]{{?\!#1}}\newcommand{\All}[1]{\Forall#1.} %quantification%%%% ``WARNING'' environment\def\dbend{\vtop to 0pt{\vss\hbox{\Huge\bf!}\vss}}\newenvironment{warn}{\medskip\medbreak\begingroup \clubpenalty=10000 \small %%WAS\baselineskip=0.9\baselineskip \noindent \ifdim\parindent > 0pt\hangindent\parindent\else\hangindent1.5em\fi \hangafter=-2 \hbox to0pt{\hskip-\hangindent\dbend\hfill}\ignorespaces}% {\par\endgroup\medbreak}%%%% Standard logical symbols\let\turn=\vdash\let\conj=\wedge\let\disj=\vee\let\imp=\rightarrow\let\bimp=\leftrightarrow\newcommand\all[1]{\forall#1.} %quantification\newcommand\ex[1]{\exists#1.}\newcommand{\pair}[1]{\langle#1\rangle}\newcommand{\lparr}{\mathopen{(\!|}}\newcommand{\rparr}{\mathclose{|\!)}}\newcommand{\fs}{\mathpunct{,\,}}\newcommand{\ty}{\mathrel{::}}\newcommand{\asn}{\mathrel{:=}}\newcommand{\more}{\ldots}\newcommand{\record}[1]{\lparr #1 \rparr}\newcommand{\dtt}{\mathord.}\newcommand\lbrakk{\mathopen{[\![}}\newcommand\rbrakk{\mathclose{]\!]}}\newcommand\List[1]{\lbrakk#1\rbrakk} %was \obj\newcommand\vpile[1]{\begin{array}{c}#1\end{array}}\newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]}\newcommand{\Text}[1]{\mbox{#1}}\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}\newcommand{\dsh}{\mathit{\dshsym}}\let\int=\cap\let\un=\cup\let\inter=\bigcap\let\union=\bigcup\def\ML{{\sc ml}}\def\OBJ{{\sc obj}}\def\AST{{\sc ast}}%macros to change the treatment of symbols\def\relsemicolon{\mathcode`\;="303B} %treat ; like a relation\def\binperiod{\mathcode`\.="213A} %treat . like a binary operator\def\binvert{\mathcode`\|="226A} %treat | like a binary operator%redefinition of \sloppy and \fussy to use \emergencystretch\def\sloppy{\tolerance2000 \hfuzz.5pt \vfuzz.5pt \emergencystretch=15pt}\def\fussy{\tolerance200 \hfuzz.1pt \vfuzz.1pt \emergencystretch=0pt}%non-bf version of description\def\descrlabel#1{\hspace\labelsep #1}\def\descr{\list{}{\labelwidth\z@ \itemindent-\leftmargin\let\makelabel\descrlabel}}\let\enddescr\endlist% The mathcodes for the letters A, ..., Z, a, ..., z are changed to% generate text italic rather than math italic by default. This makes% multi-letter identifiers look better. The mathcode for character c% is set to |"7000| (variable family) + |"400| (text italic) + |c|.%\DeclareSymbolFont{italics}{\encodingdefault}{\rmdefault}{m}{it}%\def\@setmcodes#1#2#3{{\count0=#1 \count1=#3 \loop \global\mathcode\count0=\count1 \ifnum \count0<#2 \advance\count0 by1 \advance\count1 by1 \repeat}}\@setmcodes{`A}{`Z}{"7\hexnumber@\symitalics41}\@setmcodes{`a}{`z}{"7\hexnumber@\symitalics61}