isabelle: src/Doc/isar.sty@0f7edf0853df (annotated)

7050 c70d3402fef5 checkpoint; wenzelm parents: diff changeset	1	\usepackage{ifthen}
c70d3402fef5 checkpoint; wenzelm parents: diff changeset	2
26745 93f36f5f4a35 more abstract index commands; wenzelm parents: 26744 diff changeset	3	\newcommand{\indexdef}[3]%
93f36f5f4a35 more abstract index commands; wenzelm parents: 26744 diff changeset	4	{\ifthenelse{\equal{}{#1}}{\index{#3 (#2)\|bold}}{\index{#3 (#1\ #2)\|bold}}}
93f36f5f4a35 more abstract index commands; wenzelm parents: 26744 diff changeset	5	\newcommand{\indexref}[3]{\ifthenelse{\equal{}{#1}}{\index{#3 (#2)}}{\index{#3 (#1\ #2)}}}
7138 0a17c2a93454 Isabelle/Isar macros; wenzelm parents: 7050 diff changeset	6
59346 f25442e194bf proper latex; wenzelm parents: 59343 diff changeset	7	\newcommand{\isadigitreset}{\def\isadigit##1{##1}}
f25442e194bf proper latex; wenzelm parents: 59343 diff changeset	8
59343 43281cd62cb0 tuned latex; wenzelm parents: 59003 diff changeset	9	\newcommand{\isasystem}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\isadigitreset\tt #1}}
43281cd62cb0 tuned latex; wenzelm parents: 59003 diff changeset	10	\newcommand{\isatool}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\isadigitreset\tt isabelle #1}}
28214 1e6d71cd4bf3 added isatt markup; wenzelm parents: 26868 diff changeset	11
26745 93f36f5f4a35 more abstract index commands; wenzelm parents: 26744 diff changeset	12	\newcommand{\indexoutertoken}[1]{\indexdef{}{syntax}{#1}}
93f36f5f4a35 more abstract index commands; wenzelm parents: 26744 diff changeset	13	\newcommand{\indexouternonterm}[1]{\indexdef{}{syntax}{#1}}
93f36f5f4a35 more abstract index commands; wenzelm parents: 26744 diff changeset	14	\newcommand{\indexisarelem}[1]{\indexdef{}{element}{#1}}
7170 cb8afc731bee tuned; wenzelm parents: 7138 diff changeset	15
60459 2761a2249c83 more on 'consider' and related concepts; wenzelm parents: 59346 diff changeset	16	\newcommand{\isasymIF}{\isakeyword{if}}
55143 04448228381d explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac; wenzelm parents: 51657 diff changeset	17	\newcommand{\isasymFOR}{\isakeyword{for}}
26755 84408d6ff180 added AND, IS, WHERE symbols; wenzelm parents: 26745 diff changeset	18	\newcommand{\isasymAND}{\isakeyword{and}}
84408d6ff180 added AND, IS, WHERE symbols; wenzelm parents: 26745 diff changeset	19	\newcommand{\isasymIS}{\isakeyword{is}}
84408d6ff180 added AND, IS, WHERE symbols; wenzelm parents: 26745 diff changeset	20	\newcommand{\isasymWHERE}{\isakeyword{where}}
26769 5b8382d495be added begin and imports; wenzelm parents: 26755 diff changeset	21	\newcommand{\isasymBEGIN}{\isakeyword{begin}}
5b8382d495be added begin and imports; wenzelm parents: 26755 diff changeset	22	\newcommand{\isasymIMPORTS}{\isakeyword{imports}}
26783 1651ff6a34b5 added isasymIN/STRUCTURE; wenzelm parents: 26769 diff changeset	23	\newcommand{\isasymIN}{\isakeyword{in}}
29727 cda1fb36a082 some more Isar elements; wenzelm parents: 28761 diff changeset	24	\newcommand{\isasymFIXES}{\isakeyword{fixes}}
cda1fb36a082 some more Isar elements; wenzelm parents: 28761 diff changeset	25	\newcommand{\isasymASSUMES}{\isakeyword{assumes}}
cda1fb36a082 some more Isar elements; wenzelm parents: 28761 diff changeset	26	\newcommand{\isasymSHOWS}{\isakeyword{shows}}
cda1fb36a082 some more Isar elements; wenzelm parents: 28761 diff changeset	27	\newcommand{\isasymOBTAINS}{\isakeyword{obtains}}
cda1fb36a082 some more Isar elements; wenzelm parents: 28761 diff changeset	28
cda1fb36a082 some more Isar elements; wenzelm parents: 28761 diff changeset	29	\newcommand{\isasymASSM}{\isacommand{assm}}

author	haftmann
	Fri, 14 Jun 2019 08:34:27 +0000
changeset 70333	0f7edf0853df
parent 61671	20d4cd2ceab2
child 73746	b2d47981c8dc
permissions	-rw-r--r--