# HG changeset patch # User nipkow # Date 969040745 -7200 # Node ID 4281ccea43f007c9b93e3882be4fcb4c0140c7c7 # Parent fdead18501ca290ea98516bbd035dc545b1c6742 *** empty log message *** diff -r fdead18501ca -r 4281ccea43f0 doc-src/TutorialI/CTL/CTL.thy --- a/doc-src/TutorialI/CTL/CTL.thy Fri Sep 15 19:34:28 2000 +0200 +++ b/doc-src/TutorialI/CTL/CTL.thy Fri Sep 15 19:59:05 2000 +0200 @@ -142,11 +142,11 @@ apply(intro strip); apply(induct_tac i); apply(simp); - apply(fast intro:selectI2EX); + apply(fast intro:someI2EX); apply(simp); -apply(rule selectI2EX); +apply(rule someI2EX); apply(blast); -apply(rule selectI2EX); +apply(rule someI2EX); apply(blast); by(blast); @@ -162,11 +162,11 @@ apply(intro strip); apply(induct_tac i); apply(simp); - apply(fast intro:selectI2EX); + apply(fast intro:someI2EX); apply(simp); -apply(rule selectI2EX); +apply(rule someI2EX); apply(blast); -apply(rule selectI2EX); +apply(rule someI2EX); apply(blast); by(blast); diff -r fdead18501ca -r 4281ccea43f0 doc-src/TutorialI/Recdef/document/termination.tex --- a/doc-src/TutorialI/Recdef/document/termination.tex Fri Sep 15 19:34:28 2000 +0200 +++ b/doc-src/TutorialI/Recdef/document/termination.tex Fri Sep 15 19:59:05 2000 +0200 @@ -43,7 +43,7 @@ \isacommand{consts}\ g\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline \isacommand{recdef}\ g\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline \ \ {\isachardoublequote}g{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ g{\isacharparenleft}x{\isacharcomma}y{\isacharplus}\isadigit{1}{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline -{\isacharparenleft}\isakeyword{hints}\ simp{\isacharcolon}\ termi{\isacharunderscore}lem{\isacharparenright}% +{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ termi{\isacharunderscore}lem{\isacharparenright}% \begin{isamarkuptext}% \noindent This time everything works fine. Now \isa{g{\isachardot}simps} contains precisely diff -r fdead18501ca -r 4281ccea43f0 doc-src/TutorialI/Recdef/termination.thy --- a/doc-src/TutorialI/Recdef/termination.thy Fri Sep 15 19:34:28 2000 +0200 +++ b/doc-src/TutorialI/Recdef/termination.thy Fri Sep 15 19:59:05 2000 +0200 @@ -47,7 +47,7 @@ consts g :: "nat\nat \ nat"; recdef g "measure(\(x,y). x-y)" "g(x,y) = (if x \ y then x else g(x,y+1))" -(hints simp: termi_lem) +(hints recdef_simp: termi_lem) text{*\noindent This time everything works fine. Now @{thm[source]g.simps} contains precisely diff -r fdead18501ca -r 4281ccea43f0 doc-src/TutorialI/isabelle.sty --- a/doc-src/TutorialI/isabelle.sty Fri Sep 15 19:34:28 2000 +0200 +++ b/doc-src/TutorialI/isabelle.sty Fri Sep 15 19:59:05 2000 +0200 @@ -129,4 +129,8 @@ \renewcommand{\isacharbraceright}{\emph{$\}$}}% } -\newcommand{\isabellestylesl}{\isabellestyleit\renewcommand{\isastyle}{\small\slshape}} +\newcommand{\isabellestylesl}{% +\isabellestyleit% +\renewcommand{\isastyle}{\small\sl}% +\renewcommand{\isastyleminor}{\sl}% +} diff -r fdead18501ca -r 4281ccea43f0 doc-src/TutorialI/isabellesym.sty --- a/doc-src/TutorialI/isabellesym.sty Fri Sep 15 19:34:28 2000 +0200 +++ b/doc-src/TutorialI/isabellesym.sty Fri Sep 15 19:59:05 2000 +0200 @@ -6,11 +6,17 @@ %% definitions of standard Isabelle symbols %% -\usepackage{latexsym} +% Required packages for unusual symbols -- see below for details. +%\usepackage{latexsym} %\usepackage{amssymb} +%\usepackage[english]{babel} %\usepackage[latin1]{inputenc} +%\usepackage[only,bigsqcap]{stmaryrd} +%\usepackage{wasysym} -\newcommand{\bigsqcap}{\overline{|\,\,|}} %an approximation ... +% Note: \emph is important for proper spacing in fake math mode, it +% automatically inserts italic corrections around symbols wherever +% appropriate. \newcommand{\isasymspacespace}{~~} \newcommand{\isasymGamma}{$\Gamma$} @@ -70,7 +76,7 @@ \newcommand{\isasymUnion}{\emph{$\bigcup\,$}} \newcommand{\isasymsqinter}{\emph{$\sqcap$}} \newcommand{\isasymsqunion}{\emph{$\sqcup$}} -\newcommand{\isasymSqinter}{\emph{$\bigsqcap\,$}} +\newcommand{\isasymSqinter}{\emph{$\bigsqcap\,$}} %requires stmaryrd \newcommand{\isasymSqunion}{\emph{$\bigsqcup\,$}} \newcommand{\isasymbottom}{\emph{$\bot$}} \newcommand{\isasymdoteq}{\emph{$\doteq$}} @@ -87,14 +93,14 @@ \newcommand{\isasymle}{\emph{$\le$}} \newcommand{\isasymColon}{\emph{$\mathrel{::}$}} \newcommand{\isasymleftarrow}{\emph{$\leftarrow$}} -\newcommand{\isasymmidarrow}{\emph{$-$}}%deprecated +\newcommand{\isasymmidarrow}{\emph{$\relbar$}} \newcommand{\isasymrightarrow}{\emph{$\rightarrow$}} \newcommand{\isasymLeftarrow}{\emph{$\Leftarrow$}} -\newcommand{\isasymMidarrow}{\emph{$=$}}%deprecated +\newcommand{\isasymMidarrow}{\emph{$\Relbar$}} \newcommand{\isasymRightarrow}{\emph{$\Rightarrow$}} \newcommand{\isasymfrown}{\emph{$\frown$}} \newcommand{\isasymmapsto}{\emph{$\mapsto$}} -\newcommand{\isasymleadsto}{\emph{$\leadsto$}} +\newcommand{\isasymleadsto}{\emph{$\leadsto$}} %requires latexsym \newcommand{\isasymup}{\emph{$\uparrow$}} \newcommand{\isasymdown}{\emph{$\downarrow$}} \newcommand{\isasymnotin}{\emph{$\notin$}} @@ -105,14 +111,13 @@ \newcommand{\isasymoslash}{\emph{$\oslash$}} \newcommand{\isasymsubset}{\emph{$\subset$}} \newcommand{\isasyminfinity}{\emph{$\infty$}} -\newcommand{\isasymbox}{\emph{$\Box$}} -\newcommand{\isasymdiamond}{\emph{$\Diamond$}} +\newcommand{\isasymbox}{\emph{$\Box$}} %requires latexsym +\newcommand{\isasymdiamond}{\emph{$\Diamond$}} %requires latexsym \newcommand{\isasymcirc}{\emph{$\circ$}} \newcommand{\isasymbullet}{\emph{$\bullet$}} \newcommand{\isasymparallel}{\emph{$\parallel$}} \newcommand{\isasymsurd}{\emph{$\surd$}} \newcommand{\isasymcopyright}{\emph{\copyright}} - \newcommand{\isasymplusminus}{\emph{$\pm$}} \newcommand{\isasymdiv}{\emph{$\div$}} \newcommand{\isasymlongrightarrow}{\emph{$\longrightarrow$}} @@ -121,42 +126,32 @@ \newcommand{\isasymLongrightarrow}{\emph{$\Longrightarrow$}} \newcommand{\isasymLongleftarrow}{\emph{$\Longleftarrow$}} \newcommand{\isasymLongleftrightarrow}{\emph{$\Longleftrightarrow$}} -%requires OT1 encoding: -\newcommand{\isasymbrokenbar}{\emph{\textbrokenbar}} -\newcommand{\isasymhyphen}{-} -\newcommand{\isasymmacron}{\={}} -\newcommand{\isasymexclamdown}{\emph{\textexclamdown}} -\newcommand{\isasymquestiondown}{\emph{\textquestiondown}} -%requires OT1 encoding: -\newcommand{\isasymguillemotleft}{\emph{\guillemotleft}} -%requires OT1 encoding: -\newcommand{\isasymguillemotright}{\emph{\guillemotright}} -%should be available (?): -\newcommand{\isasymdegree}{\emph{\textdegree}} -\newcommand{\isasymonesuperior}{\emph{$\mathonesuperior$}} -\newcommand{\isasymonequarter}{\emph{\textonequarter}} -\newcommand{\isasymtwosuperior}{\emph{$\mathtwosuperior$}} -\newcommand{\isasymonehalf}{\emph{\textonehalf}} -\newcommand{\isasymthreesuperior}{\emph{$\maththreesuperior$}} -\newcommand{\isasymthreequarters}{\emph{\textthreequarters}} +\newcommand{\isasymbar}{\emph{$\mid$}} +\newcommand{\isasymhyphen}{\emph{\rm-}} +\newcommand{\isasymmacron}{\emph{\rm\=\relax}} +\newcommand{\isasymexclamdown}{\emph{\rm\textexclamdown}} +\newcommand{\isasymquestiondown}{\emph{\rm\textquestiondown}} +\newcommand{\isasymguillemotleft}{\emph{\flqq}} %requires babel +\newcommand{\isasymguillemotright}{\emph{\frqq}} %requires babel +\newcommand{\isasymdegree}{\emph{\rm\textdegree}} %requires latin1 +\newcommand{\isasymonesuperior}{\emph{$\mathonesuperior$}} %requires latin1 +\newcommand{\isasymonequarter}{\emph{\rm\textonequarter}} %requires latin1 +\newcommand{\isasymtwosuperior}{\emph{$\mathtwosuperior$}} %requires latin1 +\newcommand{\isasymonehalf}{\emph{\rm\textonehalf}} %requires latin1 +\newcommand{\isasymthreesuperior}{\emph{$\maththreesuperior$}} %requires latin1 +\newcommand{\isasymthreequarters}{\emph{\rm\textthreequarters}} %requires latin1 \newcommand{\isasymparagraph}{\emph{\P}} -\newcommand{\isasymregistered}{\emph{\textregistered}} -%should be available (?): -\newcommand{\isasymordfeminine}{\emph{\textordfeminine}} -%should be available (?): -\newcommand{\isasymordmasculine}{\emph{\textordmasculine}} -\newcommand{\isasymsection}{\S} +\newcommand{\isasymregistered}{\emph{\rm\textregistered}} +\newcommand{\isasymordfeminine}{\emph{\rm\textordfeminine}} +\newcommand{\isasymordmasculine}{\emph{\rm\textordmasculine}} +\newcommand{\isasymsection}{\emph{\S}} \newcommand{\isasympounds}{\emph{$\pounds$}} -%requires OT1 encoding: -\newcommand{\isasymyen}{\emph{\textyen}} -%requires OT1 encoding: -\newcommand{\isasymcent}{\emph{\textcent}} -%requires OT1 encoding: -\newcommand{\isasymcurrency}{\emph{\textcurrency}} +\newcommand{\isasymyen}{\emph{\yen}} %requires amssymb +\newcommand{\isasymcent}{\emph{\cent}} %requires wasysym +\newcommand{\isasymcurrency}{\emph{\currency}} %requires wasysym \newcommand{\isasymlbrace}{\emph{$\mathopen{\lbrace\mkern-4.5mu\mid}$}} \newcommand{\isasymrbrace}{\emph{$\mathclose{\mid\mkern-4.5mu\rbrace}$}} \newcommand{\isasymtop}{\emph{$\top$}} - \newcommand{\isasymcong}{\emph{$\cong$}} \newcommand{\isasymclubsuit}{\emph{$\clubsuit$}} \newcommand{\isasymdiamondsuit}{\emph{$\diamondsuit$}} @@ -178,7 +173,7 @@ \newcommand{\isasymLeftrightarrow}{\emph{$\Leftrightarrow$}} \newcommand{\isasymUparrow}{\emph{$\Uparrow$}} \newcommand{\isasymDownarrow}{\emph{$\Downarrow$}} -\newcommand{\isasymlozenge}{\emph{$\lozenge$}} +\newcommand{\isasymlozenge}{\emph{$\lozenge$}} %requires amssym \newcommand{\isasymlangle}{\emph{$\langle$}} \newcommand{\isasymrangle}{\emph{$\rangle$}} \newcommand{\isasymSum}{\emph{$\sum\,$}} @@ -196,7 +191,7 @@ \newcommand{\isasymnatural}{\emph{$\natural$}} \newcommand{\isasymflat}{\emph{$\flat$}} \newcommand{\isasymamalg}{\emph{$\amalg$}} -\newcommand{\isasymmho}{\emph{$\mho$}} +\newcommand{\isasymmho}{\emph{$\mho$}} %requires latexsym \newcommand{\isasymupdownarrow}{\emph{$\updownarrow$}} \newcommand{\isasymlongmapsto}{\emph{$\longmapsto$}} \newcommand{\isasymUpdownarrow}{\emph{$\Updownarrow$}} @@ -214,7 +209,7 @@ \newcommand{\isasymodot}{\emph{$\odot$}} \newcommand{\isasymsupset}{\emph{$\supset$}} \newcommand{\isasymsupseteq}{\emph{$\supseteq$}} -\newcommand{\isasymsqsupset}{\emph{$\sqsupset$}} +\newcommand{\isasymsqsupset}{\emph{$\sqsupset$}} %requires latexsym \newcommand{\isasymsqsupseteq}{\emph{$\sqsupseteq$}} \newcommand{\isasymll}{\emph{$\ll$}} \newcommand{\isasymgg}{\emph{$\gg$}} @@ -225,17 +220,17 @@ \newcommand{\isasymOr}{\emph{$\bigvee$}} \newcommand{\isasymbiguplus}{\emph{$\biguplus$}} \newcommand{\isasymddagger}{\emph{$\ddagger$}} -\newcommand{\isasymJoin}{\emph{$\Join$}} +\newcommand{\isasymJoin}{\emph{$\Join$}} %requires latexsym \newcommand{\isasymbool}{\emph{$\mathrm{I}\mkern-3.8mu\mathrm{B}$}} \newcommand{\isasymcomplex}{\emph{$\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu$}} \newcommand{\isasymnat}{\emph{$\mathrm{I}\mkern-3.8mu\mathrm{N}$}} \newcommand{\isasymrat}{\emph{$\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu$}} \newcommand{\isasymreal}{\emph{$\mathrm{I}\mkern-3.8mu\mathrm{R}$}} \newcommand{\isasymint}{\emph{$\mathsf{Z}\mkern-7.5mu\mathsf{Z}$}} - -%require amssymb: -\newcommand{\isasymlesssim}{\emph{$\lesssim$}} -\newcommand{\isasymgreatersim}{\emph{$\gtrsim$}} -\newcommand{\isasymlessapprox}{\emph{$\lessapprox$}} -\newcommand{\isasymgreaterapprox}{\emph{$\gtrapprox$}} -\newcommand{\isasymtriangleq}{\emph{$\triangleq$}} +\newcommand{\isasymlesssim}{\emph{$\lesssim$}} %requires amssymb +\newcommand{\isasymgreatersim}{\emph{$\gtrsim$}} %requires amssymb +\newcommand{\isasymlessapprox}{\emph{$\lessapprox$}} %requires amssymb +\newcommand{\isasymgreaterapprox}{\emph{$\gtrapprox$}} %requires amssymb +\newcommand{\isasymtriangleq}{\emph{$\triangleq$}} %requires amssymb +\newcommand{\isasymlparr}{\emph{$\mathopen{(\mkern-3mu\mid}$}} +\newcommand{\isasymrparr}{\emph{$\mathclose{\mid\mkern-3mu)}$}}