lexing: thys2/Journal/isabelle.sty@6e97f4aa7cd0 (annotated)

369 e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	1	%%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	2	%% macros for Isabelle generated LaTeX output
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	3	%%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	4
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	5	%%% Simple document preparation (based on theory token language and symbols)
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	6
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	7	% isabelle environments
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	8
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	9	\newcommand{\isabellecontext}{UNKNOWN}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	10	\newcommand{\setisabellecontext}[1]{\def\isabellecontext{#1}}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	11
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	12	\newcommand{\isastyle}{\UNDEF}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	13	\newcommand{\isastylett}{\UNDEF}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	14	\newcommand{\isastyleminor}{\UNDEF}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	15	\newcommand{\isastyleminortt}{\UNDEF}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	16	\newcommand{\isastylescript}{\UNDEF}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	17	\newcommand{\isastyletext}{\normalsize\normalfont\rmfamily}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	18	\newcommand{\isastyletxt}{\normalfont\rmfamily}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	19	\newcommand{\isastylecmt}{\normalfont\rmfamily}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	20
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	21	\newcommand{\isaspacing}{%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	22	\sfcode 42 1000 % .
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	23	\sfcode 63 1000 % ?
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	24	\sfcode 33 1000 % !
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	25	\sfcode 58 1000 % :
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	26	\sfcode 59 1000 % ;
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	27	\sfcode 44 1000 % ,
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	28	}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	29
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	30	%symbol markup -- \emph achieves decent spacing via italic corrections
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	31	\newcommand{\isamath}[1]{\emph{$#1$}}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	32	\newcommand{\isatext}[1]{\emph{#1}}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	33	\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isaspacing\isastylescript##1}}}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	34	\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	35	\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	36	\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isaspacing\isastylescript}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	37	\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	38	\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isaspacing\isastylescript}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	39	\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	40	\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	41
382 aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	42	%blackboard-bold (requires font txmia from pxfonts)
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	43	\DeclareSymbolFont{bbbfont}{U}{txmia}{m}{it}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	44	\SetSymbolFont{bbbfont}{bold}{U}{txmia}{bx}{it}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	45	\DeclareMathSymbol{\bbbA}{\mathord}{bbbfont}{129}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	46	\DeclareMathSymbol{\bbbB}{\mathord}{bbbfont}{130}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	47	\DeclareMathSymbol{\bbbC}{\mathord}{bbbfont}{131}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	48	\DeclareMathSymbol{\bbbD}{\mathord}{bbbfont}{132}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	49	\DeclareMathSymbol{\bbbE}{\mathord}{bbbfont}{133}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	50	\DeclareMathSymbol{\bbbF}{\mathord}{bbbfont}{134}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	51	\DeclareMathSymbol{\bbbG}{\mathord}{bbbfont}{135}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	52	\DeclareMathSymbol{\bbbH}{\mathord}{bbbfont}{136}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	53	\DeclareMathSymbol{\bbbI}{\mathord}{bbbfont}{137}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	54	\DeclareMathSymbol{\bbbJ}{\mathord}{bbbfont}{138}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	55	\DeclareMathSymbol{\bbbK}{\mathord}{bbbfont}{139}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	56	\DeclareMathSymbol{\bbbL}{\mathord}{bbbfont}{140}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	57	\DeclareMathSymbol{\bbbM}{\mathord}{bbbfont}{141}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	58	\DeclareMathSymbol{\bbbN}{\mathord}{bbbfont}{142}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	59	\DeclareMathSymbol{\bbbO}{\mathord}{bbbfont}{143}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	60	\DeclareMathSymbol{\bbbP}{\mathord}{bbbfont}{144}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	61	\DeclareMathSymbol{\bbbQ}{\mathord}{bbbfont}{145}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	62	\DeclareMathSymbol{\bbbR}{\mathord}{bbbfont}{146}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	63	\DeclareMathSymbol{\bbbS}{\mathord}{bbbfont}{147}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	64	\DeclareMathSymbol{\bbbT}{\mathord}{bbbfont}{148}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	65	\DeclareMathSymbol{\bbbU}{\mathord}{bbbfont}{149}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	66	\DeclareMathSymbol{\bbbV}{\mathord}{bbbfont}{150}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	67	\DeclareMathSymbol{\bbbW}{\mathord}{bbbfont}{151}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	68	\DeclareMathSymbol{\bbbX}{\mathord}{bbbfont}{152}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	69	\DeclareMathSymbol{\bbbY}{\mathord}{bbbfont}{153}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	70	\DeclareMathSymbol{\bbbZ}{\mathord}{bbbfont}{154}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	71
369 e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	72	\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	73
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	74	\newdimen\isa@parindent\newdimen\isa@parskip
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	75
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	76	\newenvironment{isabellebody}{%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	77	\isamarkuptrue\par%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	78	\isa@parindent\parindent\parindent0pt%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	79	\isa@parskip\parskip\parskip0pt%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	80	\isaspacing\isastyle}{\par}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	81
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	82	\newenvironment{isabellebodytt}{%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	83	\isamarkuptrue\par%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	84	\isa@parindent\parindent\parindent0pt%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	85	\isa@parskip\parskip\parskip0pt%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	86	\isaspacing\isastylett}{\par}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	87
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	88	\newenvironment{isabelle}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	89	{\begin{trivlist}\begin{isabellebody}\item\relax}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	90	{\end{isabellebody}\end{trivlist}}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	91
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	92	\newenvironment{isabellett}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	93	{\begin{trivlist}\begin{isabellebodytt}\item\relax}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	94	{\end{isabellebodytt}\end{trivlist}}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	95
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	96	\newcommand{\isa}[1]{\emph{\isaspacing\isastyleminor #1}}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	97	\newcommand{\isatt}[1]{\emph{\isaspacing\isastyleminortt #1}}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	98
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	99	\newcommand{\isaindent}[1]{\hphantom{#1}}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	100	\newcommand{\isanewline}{\mbox{}\par\mbox{}}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	101	\newcommand{\isasep}{}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	102	\newcommand{\isadigit}[1]{#1}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	103
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	104	\newcommand{\isachardefaults}{%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	105	\def\isacharbell{\isamath{\bigbox}}%requires stmaryrd
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	106	\chardef\isacharbang=`\!%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	107	\chardef\isachardoublequote=`\"%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	108	\chardef\isachardoublequoteopen=`\"%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	109	\chardef\isachardoublequoteclose=`\"%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	110	\chardef\isacharhash=`\#%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	111	\chardef\isachardollar=`\$%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	112	\chardef\isacharpercent=`\%%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	113	\chardef\isacharampersand=`\&%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	114	\chardef\isacharprime=`\'%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	115	\chardef\isacharparenleft=`\(%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	116	\chardef\isacharparenright=`\)%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	117	\chardef\isacharasterisk=`\*%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	118	\chardef\isacharplus=`\+%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	119	\chardef\isacharcomma=`\,%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	120	\chardef\isacharminus=`\-%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	121	\chardef\isachardot=`\.%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	122	\chardef\isacharslash=`\/%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	123	\chardef\isacharcolon=`\:%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	124	\chardef\isacharsemicolon=`\;%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	125	\chardef\isacharless=`\<%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	126	\chardef\isacharequal=`\=%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	127	\chardef\isachargreater=`\>%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	128	\chardef\isacharquery=`\?%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	129	\chardef\isacharat=`\@%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	130	\chardef\isacharbrackleft=`\[%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	131	\chardef\isacharbackslash=`\\%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	132	\chardef\isacharbrackright=`\]%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	133	\chardef\isacharcircum=`\^%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	134	\chardef\isacharunderscore=`\_%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	135	\def\isacharunderscorekeyword{\_}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	136	\chardef\isacharbackquote=`\`%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	137	\chardef\isacharbackquoteopen=`\`%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	138	\chardef\isacharbackquoteclose=`\`%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	139	\chardef\isacharbraceleft=`\{%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	140	\chardef\isacharbar=`\\|%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	141	\chardef\isacharbraceright=`\}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	142	\chardef\isachartilde=`\~%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	143	\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	144	\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
382 aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	145	\def\isacartoucheopen{\isatext{\guilsinglleft}}%
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	146	\def\isacartoucheclose{\isatext{\guilsinglright}}%
369 e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	147	}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	148
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	149
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	150	% keyword and section markup
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	151
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	152	\newcommand{\isakeyword}[1]
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	153	{\emph{\normalfont\bfseries\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	154	\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	155	\newcommand{\isacommand}[1]{\isakeyword{#1}}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	156
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	157	\newcommand{\isakeywordcontrol}[1]
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	158	{\emph{\normalfont\bfseries\itshape\def\isacharunderscore{\isacharunderscorekeyword}#1\,}}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	159
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	160	\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	161	\newcommand{\isamarkupsection}[1]{\section{#1}}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	162	\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	163	\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	164	\newcommand{\isamarkupparagraph}[1]{\paragraph{#1}}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	165	\newcommand{\isamarkupsubparagraph}[1]{\subparagraph{#1}}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	166
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	167	\newif\ifisamarkup
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	168	\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	169	\newcommand{\isaendpar}{\par\medskip}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	170	\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	171	\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	172	\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	173	\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	174
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	175
382 aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	176	% index entries
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	177
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	178	\newcommand{\isaindexdef}[1]{\textbf{#1}}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	179	\newcommand{\isaindexref}[1]{#1}
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	180
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	181
369 e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	182	% styles
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	183
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	184	\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	185
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	186	\newcommand{\isabellestyledefault}{%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	187	\def\isastyle{\small\normalfont\ttfamily\slshape}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	188	\def\isastylett{\small\normalfont\ttfamily}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	189	\def\isastyleminor{\small\normalfont\ttfamily\slshape}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	190	\def\isastyleminortt{\small\normalfont\ttfamily}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	191	\def\isastylescript{\footnotesize\normalfont\ttfamily\slshape}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	192	\isachardefaults%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	193	}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	194	\isabellestyledefault
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	195
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	196	\newcommand{\isabellestylett}{%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	197	\def\isastyle{\small\normalfont\ttfamily}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	198	\def\isastylett{\small\normalfont\ttfamily}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	199	\def\isastyleminor{\small\normalfont\ttfamily}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	200	\def\isastyleminortt{\small\normalfont\ttfamily}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	201	\def\isastylescript{\footnotesize\normalfont\ttfamily}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	202	\isachardefaults%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	203	}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	204
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	205	\newcommand{\isabellestyleit}{%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	206	\def\isastyle{\small\normalfont\itshape}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	207	\def\isastylett{\small\normalfont\ttfamily}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	208	\def\isastyleminor{\normalfont\itshape}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	209	\def\isastyleminortt{\normalfont\ttfamily}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	210	\def\isastylescript{\footnotesize\normalfont\itshape}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	211	\isachardefaults%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	212	\def\isacharunderscorekeyword{\mbox{-}}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	213	\def\isacharbang{\isamath{!}}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	214	\def\isachardoublequote{}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	215	\def\isachardoublequoteopen{}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	216	\def\isachardoublequoteclose{}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	217	\def\isacharhash{\isamath{\#}}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	218	\def\isachardollar{\isamath{\$}}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	219	\def\isacharpercent{\isamath{\%}}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	220	\def\isacharampersand{\isamath{\&}}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	221	\def\isacharprime{\isamath{\mskip2mu{'}\mskip-2mu}}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	222	\def\isacharparenleft{\isamath{(}}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	223	\def\isacharparenright{\isamath{)}}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	224	\def\isacharasterisk{\isamath{*}}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	225	\def\isacharplus{\isamath{+}}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	226	\def\isacharcomma{\isamath{\mathord,}}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	227	\def\isacharminus{\isamath{-}}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	228	\def\isachardot{\isamath{\mathord.}}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	229	\def\isacharslash{\isamath{/}}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	230	\def\isacharcolon{\isamath{\mathord:}}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	231	\def\isacharsemicolon{\isamath{\mathord;}}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	232	\def\isacharless{\isamath{<}}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	233	\def\isacharequal{\isamath{=}}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	234	\def\isachargreater{\isamath{>}}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	235	\def\isacharat{\isamath{@}}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	236	\def\isacharbrackleft{\isamath{[}}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	237	\def\isacharbackslash{\isamath{\backslash}}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	238	\def\isacharbrackright{\isamath{]}}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	239	\def\isacharunderscore{\mbox{-}}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	240	\def\isacharbraceleft{\isamath{\{}}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	241	\def\isacharbar{\isamath{\mid}}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	242	\def\isacharbraceright{\isamath{\}}}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	243	\def\isachartilde{\isamath{{}\sp{\sim}}}%
382 aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	244	\def\isacharbackquoteopen{\isatext{\guilsinglleft}}%
aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	245	\def\isacharbackquoteclose{\isatext{\guilsinglright}}%
369 e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	246	}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	247
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	248	\newcommand{\isabellestyleliteral}{%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	249	\isabellestyleit%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	250	\def\isacharunderscore{\_}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	251	\def\isacharunderscorekeyword{\_}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	252	\chardef\isacharbackquoteopen=`\`%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	253	\chardef\isacharbackquoteclose=`\`%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	254	}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	255
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	256	\newcommand{\isabellestyleliteralunderscore}{%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	257	\isabellestyleliteral%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	258	\def\isacharunderscore{\textunderscore}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	259	\def\isacharunderscorekeyword{\textunderscore}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	260	}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	261
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	262	\newcommand{\isabellestylesl}{%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	263	\isabellestyleit%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	264	\def\isastyle{\small\normalfont\slshape}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	265	\def\isastylett{\small\normalfont\ttfamily}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	266	\def\isastyleminor{\normalfont\slshape}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	267	\def\isastyleminortt{\normalfont\ttfamily}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	268	\def\isastylescript{\footnotesize\normalfont\slshape}%
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	269	}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	270
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	271
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	272	% cancel text
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	273
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	274	\usepackage[normalem]{ulem}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	275	\newcommand{\isamarkupcancel}[1]{\isa{\xout{#1}}}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	276
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	277
382 aef235b965bb deleted .tex files from Journal - they are recreated Christian Urban <christian.urban@kcl.ac.uk>* parents: 369 diff changeset	278	% tags
369 e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	279
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	280	\newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	281
e00950ba4514 added all files in Journal folder Chengsong parents: diff changeset	282	\IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}

author	Chengsong
	Thu, 23 Jun 2022 16:59:58 +0100
changeset 546	6e97f4aa7cd0
parent 382	aef235b965bb
permissions	-rw-r--r--