isabelle: src/Doc/isar.sty@d20f19f54789 (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
28214 1e6d71cd4bf3 added isatt markup; wenzelm parents: 26868 diff changeset	7	\newcommand{\isatt}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\tt #1}}
48602 342ca8f3197b more uniform usage of "isabelle tool"; wenzelm parents: 29727 diff changeset	8	\newcommand{\isatool}[1]{{\def\isacharminus{-}\def\isacharunderscore{\_}\tt isabelle #1}}
28214 1e6d71cd4bf3 added isatt markup; wenzelm parents: 26868 diff changeset	9
26745 93f36f5f4a35 more abstract index commands; wenzelm parents: 26744 diff changeset	10	\newcommand{\indexoutertoken}[1]{\indexdef{}{syntax}{#1}}
93f36f5f4a35 more abstract index commands; wenzelm parents: 26744 diff changeset	11	\newcommand{\indexouternonterm}[1]{\indexdef{}{syntax}{#1}}
93f36f5f4a35 more abstract index commands; wenzelm parents: 26744 diff changeset	12	\newcommand{\indexisarelem}[1]{\indexdef{}{element}{#1}}
7170 cb8afc731bee tuned; wenzelm parents: 7138 diff changeset	13
55143 04448228381d explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac; wenzelm parents: 51657 diff changeset	14	\newcommand{\isasymFOR}{\isakeyword{for}}
26755 84408d6ff180 added AND, IS, WHERE symbols; wenzelm parents: 26745 diff changeset	15	\newcommand{\isasymAND}{\isakeyword{and}}
84408d6ff180 added AND, IS, WHERE symbols; wenzelm parents: 26745 diff changeset	16	\newcommand{\isasymIS}{\isakeyword{is}}
84408d6ff180 added AND, IS, WHERE symbols; wenzelm parents: 26745 diff changeset	17	\newcommand{\isasymWHERE}{\isakeyword{where}}
26769 5b8382d495be added begin and imports; wenzelm parents: 26755 diff changeset	18	\newcommand{\isasymBEGIN}{\isakeyword{begin}}
5b8382d495be added begin and imports; wenzelm parents: 26755 diff changeset	19	\newcommand{\isasymIMPORTS}{\isakeyword{imports}}
26783 1651ff6a34b5 added isasymIN/STRUCTURE; wenzelm parents: 26769 diff changeset	20	\newcommand{\isasymIN}{\isakeyword{in}}
29727 cda1fb36a082 some more Isar elements; wenzelm parents: 28761 diff changeset	21	\newcommand{\isasymFIXES}{\isakeyword{fixes}}
cda1fb36a082 some more Isar elements; wenzelm parents: 28761 diff changeset	22	\newcommand{\isasymASSUMES}{\isakeyword{assumes}}
cda1fb36a082 some more Isar elements; wenzelm parents: 28761 diff changeset	23	\newcommand{\isasymSHOWS}{\isakeyword{shows}}
cda1fb36a082 some more Isar elements; wenzelm parents: 28761 diff changeset	24	\newcommand{\isasymOBTAINS}{\isakeyword{obtains}}
cda1fb36a082 some more Isar elements; wenzelm parents: 28761 diff changeset	25
cda1fb36a082 some more Isar elements; wenzelm parents: 28761 diff changeset	26	\newcommand{\isasymASSM}{\isacommand{assm}}

author	blanchet
	Fri, 16 May 2014 19:13:50 +0200
changeset 56984	d20f19f54789
parent 55143	04448228381d
child 58716	23a380cc45f4
permissions	-rw-r--r--