updated
authorwenzelm
Thu Feb 01 20:48:58 2001 +0100 (2001-02-01)
changeset 110236e6c8d1ec89e
parent 11022 72a76580ed2f
child 11024 23bf8d787b04
updated
doc-src/TutorialI/Recdef/document/Induction.tex
doc-src/TutorialI/isabellesym.sty
     1.1 --- a/doc-src/TutorialI/Recdef/document/Induction.tex	Thu Feb 01 20:45:54 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Recdef/document/Induction.tex	Thu Feb 01 20:48:58 2001 +0100
     1.3 @@ -49,7 +49,7 @@
     1.4  
     1.5  In general, the format of invoking recursion induction is
     1.6  \begin{quote}
     1.7 -\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac\ }$x@1 \dots x@n$ \isa{rule{\isacharcolon}} $f$\isa{{\isachardot}induct{\isacharparenright}}
     1.8 +\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac}$x@1 \dots x@n$ \isa{rule{\isacharcolon}} $f$\isa{{\isachardot}induct{\isacharparenright}}
     1.9  \end{quote}\index{*induct_tac}%
    1.10  where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
    1.11  name of a function that takes an $n$-tuple. Usually the subgoal will
     2.1 --- a/doc-src/TutorialI/isabellesym.sty	Thu Feb 01 20:45:54 2001 +0100
     2.2 +++ b/doc-src/TutorialI/isabellesym.sty	Thu Feb 01 20:48:58 2001 +0100
     2.3 @@ -12,6 +12,7 @@
     2.4  %\usepackage[latin1]{inputenc}
     2.5  %\usepackage[only,bigsqcap]{stmaryrd}
     2.6  %\usepackage{wasysym}
     2.7 +%\usepackage{eufrak}
     2.8  
     2.9  
    2.10  % symbol definitions
    2.11 @@ -68,6 +69,58 @@
    2.12  \newcommand{\isasymx}{\isamath{\mathrm{x}}}
    2.13  \newcommand{\isasymy}{\isamath{\mathrm{y}}}
    2.14  \newcommand{\isasymz}{\isamath{\mathrm{z}}}
    2.15 +\newcommand{\isasymAA}{\isamath{\mathfrak{A}}}  %requires eufrak
    2.16 +\newcommand{\isasymBB}{\isamath{\mathfrak{B}}}  %requires eufrak
    2.17 +\newcommand{\isasymCC}{\isamath{\mathfrak{C}}}  %requires eufrak
    2.18 +\newcommand{\isasymDD}{\isamath{\mathfrak{D}}}  %requires eufrak
    2.19 +\newcommand{\isasymEE}{\isamath{\mathfrak{E}}}  %requires eufrak
    2.20 +\newcommand{\isasymFF}{\isamath{\mathfrak{F}}}  %requires eufrak
    2.21 +\newcommand{\isasymGG}{\isamath{\mathfrak{G}}}  %requires eufrak
    2.22 +\newcommand{\isasymHH}{\isamath{\mathfrak{H}}}  %requires eufrak
    2.23 +\newcommand{\isasymII}{\isamath{\mathfrak{I}}}  %requires eufrak
    2.24 +\newcommand{\isasymJJ}{\isamath{\mathfrak{J}}}  %requires eufrak
    2.25 +\newcommand{\isasymKK}{\isamath{\mathfrak{K}}}  %requires eufrak
    2.26 +\newcommand{\isasymLL}{\isamath{\mathfrak{L}}}  %requires eufrak
    2.27 +\newcommand{\isasymMM}{\isamath{\mathfrak{M}}}  %requires eufrak
    2.28 +\newcommand{\isasymNN}{\isamath{\mathfrak{N}}}  %requires eufrak
    2.29 +\newcommand{\isasymOO}{\isamath{\mathfrak{O}}}  %requires eufrak
    2.30 +\newcommand{\isasymPP}{\isamath{\mathfrak{P}}}  %requires eufrak
    2.31 +\newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}}  %requires eufrak
    2.32 +\newcommand{\isasymRR}{\isamath{\mathfrak{R}}}  %requires eufrak
    2.33 +\newcommand{\isasymSS}{\isamath{\mathfrak{S}}}  %requires eufrak
    2.34 +\newcommand{\isasymTT}{\isamath{\mathfrak{T}}}  %requires eufrak
    2.35 +\newcommand{\isasymUU}{\isamath{\mathfrak{U}}}  %requires eufrak
    2.36 +\newcommand{\isasymVV}{\isamath{\mathfrak{V}}}  %requires eufrak
    2.37 +\newcommand{\isasymWW}{\isamath{\mathfrak{W}}}  %requires eufrak
    2.38 +\newcommand{\isasymXX}{\isamath{\mathfrak{X}}}  %requires eufrak
    2.39 +\newcommand{\isasymYY}{\isamath{\mathfrak{Y}}}  %requires eufrak
    2.40 +\newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}}  %requires eufrak
    2.41 +\newcommand{\isasymaa}{\isamath{\mathfrak{a}}}  %requires eufrak
    2.42 +\newcommand{\isasymbb}{\isamath{\mathfrak{b}}}  %requires eufrak
    2.43 +\newcommand{\isasymcc}{\isamath{\mathfrak{c}}}  %requires eufrak
    2.44 +\newcommand{\isasymdd}{\isamath{\mathfrak{d}}}  %requires eufrak
    2.45 +\newcommand{\isasymee}{\isamath{\mathfrak{e}}}  %requires eufrak
    2.46 +\newcommand{\isasymff}{\isamath{\mathfrak{f}}}  %requires eufrak
    2.47 +\newcommand{\isasymgg}{\isamath{\mathfrak{g}}}  %requires eufrak
    2.48 +\newcommand{\isasymhh}{\isamath{\mathfrak{h}}}  %requires eufrak
    2.49 +\newcommand{\isasymii}{\isamath{\mathfrak{i}}}  %requires eufrak
    2.50 +\newcommand{\isasymjj}{\isamath{\mathfrak{j}}}  %requires eufrak
    2.51 +\newcommand{\isasymkk}{\isamath{\mathfrak{k}}}  %requires eufrak
    2.52 +\newcommand{\isasymll}{\isamath{\mathfrak{l}}}  %requires eufrak
    2.53 +\newcommand{\isasymmm}{\isamath{\mathfrak{m}}}  %requires eufrak
    2.54 +\newcommand{\isasymnn}{\isamath{\mathfrak{n}}}  %requires eufrak
    2.55 +\newcommand{\isasymoo}{\isamath{\mathfrak{o}}}  %requires eufrak
    2.56 +\newcommand{\isasympp}{\isamath{\mathfrak{p}}}  %requires eufrak
    2.57 +\newcommand{\isasymqq}{\isamath{\mathfrak{q}}}  %requires eufrak
    2.58 +\newcommand{\isasymrr}{\isamath{\mathfrak{r}}}  %requires eufrak
    2.59 +\newcommand{\isasymss}{\isamath{\mathfrak{s}}}  %requires eufrak
    2.60 +\newcommand{\isasymtt}{\isamath{\mathfrak{t}}}  %requires eufrak
    2.61 +\newcommand{\isasymuu}{\isamath{\mathfrak{u}}}  %requires eufrak
    2.62 +\newcommand{\isasymvv}{\isamath{\mathfrak{v}}}  %requires eufrak
    2.63 +\newcommand{\isasymww}{\isamath{\mathfrak{w}}}  %requires eufrak
    2.64 +\newcommand{\isasymxx}{\isamath{\mathfrak{x}}}  %requires eufrak
    2.65 +\newcommand{\isasymyy}{\isamath{\mathfrak{y}}}  %requires eufrak
    2.66 +\newcommand{\isasymzz}{\isamath{\mathfrak{z}}}  %requires eufrak
    2.67  \newcommand{\isasymalpha}{\isamath{\alpha}}
    2.68  \newcommand{\isasymbeta}{\isamath{\beta}}
    2.69  \newcommand{\isasymgamma}{\isamath{\gamma}}
    2.70 @@ -170,8 +223,8 @@
    2.71  \newcommand{\isasymsurd}{\isamath{\surd}}
    2.72  \newcommand{\isasymle}{\isamath{\le}}
    2.73  \newcommand{\isasymge}{\isamath{\ge}}
    2.74 -\newcommand{\isasymll}{\isamath{\ll}}
    2.75 -\newcommand{\isasymgg}{\isamath{\gg}}
    2.76 +\newcommand{\isasymlless}{\isamath{\ll}}
    2.77 +\newcommand{\isasymggreater}{\isamath{\gg}}
    2.78  \newcommand{\isasymlesssim}{\isamath{\lesssim}}  %requires amssymb
    2.79  \newcommand{\isasymgreatersim}{\isamath{\gtrsim}}  %requires amssymb
    2.80  \newcommand{\isasymlessapprox}{\isamath{\lessapprox}}  %requires amssymb