isabelle: doc-src/IsarRef/isar-ref.tex@fe35b72b9ef0 (annotated)

7836 7a9270282fd3 a4paper; wenzelm parents: 7532 diff changeset	1	\documentclass[12pt,a4paper,fleqn]{report}
28838 d5db6dfcb34a moved table of standard Isabelle symbols to isar-ref manual; wenzelm parents: 28773 diff changeset	2	\usepackage{amssymb}
d5db6dfcb34a moved table of standard Isabelle symbols to isar-ref manual; wenzelm parents: 28773 diff changeset	3	\usepackage[greek,english]{babel}
d5db6dfcb34a moved table of standard Isabelle symbols to isar-ref manual; wenzelm parents: 28773 diff changeset	4	\usepackage[latin1]{inputenc}
d5db6dfcb34a moved table of standard Isabelle symbols to isar-ref manual; wenzelm parents: 28773 diff changeset	5	\usepackage[only,bigsqcap]{stmaryrd}
d5db6dfcb34a moved table of standard Isabelle symbols to isar-ref manual; wenzelm parents: 28773 diff changeset	6	\usepackage{textcomp}
d5db6dfcb34a moved table of standard Isabelle symbols to isar-ref manual; wenzelm parents: 28773 diff changeset	7	\usepackage{latexsym}
d5db6dfcb34a moved table of standard Isabelle symbols to isar-ref manual; wenzelm parents: 28773 diff changeset	8	\usepackage{graphicx}
d5db6dfcb34a moved table of standard Isabelle symbols to isar-ref manual; wenzelm parents: 28773 diff changeset	9	\let\intorig=\int %iman.sty redefines \int
26738 615e1a86787b basic setup for generated document (cf. ../IsarImplementation); wenzelm parents: 18021 diff changeset	10	\usepackage{../iman,../extra,../isar,../proof}
26862 a79d7d5f1d06 added local copy of underscore.sty; wenzelm parents: 26858 diff changeset	11	\usepackage[nohyphen,strings]{../underscore}
26906 6e8152678e06 use ../isabelle.sty, ../isabellesym.sty; wenzelm parents: 26904 diff changeset	12	\usepackage{../isabelle,../isabellesym}
26738 615e1a86787b basic setup for generated document (cf. ../IsarImplementation); wenzelm parents: 18021 diff changeset	13	\usepackage{../ttbox,,../rail,../railsetup}
28773 39b4cedb8433 updated and elaborated Pure grammer; wenzelm parents: 28762 diff changeset	14	\usepackage{supertabular}
26738 615e1a86787b basic setup for generated document (cf. ../IsarImplementation); wenzelm parents: 18021 diff changeset	15	\usepackage{style}
615e1a86787b basic setup for generated document (cf. ../IsarImplementation); wenzelm parents: 18021 diff changeset	16	\usepackage{../pdfsetup}
7046 9f755ff43cff skeleton only; wenzelm parents: diff changeset	17
26741 eb15fd4cd1ad converted intro.tex to Thy/intro.thy; wenzelm parents: 26738 diff changeset	18	\hyphenation{Isabelle}
eb15fd4cd1ad converted intro.tex to Thy/intro.thy; wenzelm parents: 26738 diff changeset	19	\hyphenation{Isar}
eb15fd4cd1ad converted intro.tex to Thy/intro.thy; wenzelm parents: 26738 diff changeset	20
eb15fd4cd1ad converted intro.tex to Thy/intro.thy; wenzelm parents: 26738 diff changeset	21	\isadroptag{theory}
7046 9f755ff43cff skeleton only; wenzelm parents: diff changeset	22	\title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
26870 94bedbb34b92 misc reorganization; wenzelm parents: 26869 diff changeset	23	\author{\emph{Makarius Wenzel} \\[3ex]
94bedbb34b92 misc reorganization; wenzelm parents: 26869 diff changeset	24	With Contributions by
94bedbb34b92 misc reorganization; wenzelm parents: 26869 diff changeset	25	Clemens Ballarin,
94bedbb34b92 misc reorganization; wenzelm parents: 26869 diff changeset	26	Stefan Berghofer, \\
30569 696f93184f0d tuned interpunctation haftmann parents: 30242 diff changeset	27	Timothy Bourke,
27038 854c61598628 more contributors; wenzelm parents: 27037 diff changeset	28	Lucas Dixon,
30185 6889bfc03804 updated contributors; wenzelm parents: 30116 diff changeset	29	Florian Haftmann, \\
6889bfc03804 updated contributors; wenzelm parents: 30116 diff changeset	30	Gerwin Klein,
27038 854c61598628 more contributors; wenzelm parents: 27037 diff changeset	31	Alexander Krauss,
30185 6889bfc03804 updated contributors; wenzelm parents: 30116 diff changeset	32	Tobias Nipkow, \\
6889bfc03804 updated contributors; wenzelm parents: 30116 diff changeset	33	David von Oheimb,
27038 854c61598628 more contributors; wenzelm parents: 27037 diff changeset	34	Larry Paulson,
26870 94bedbb34b92 misc reorganization; wenzelm parents: 26869 diff changeset	35	and Sebastian Skalberg
94bedbb34b92 misc reorganization; wenzelm parents: 26869 diff changeset	36	}
7046 9f755ff43cff skeleton only; wenzelm parents: diff changeset	37
7050 c70d3402fef5 checkpoint; wenzelm parents: 7046 diff changeset	38	\makeindex
c70d3402fef5 checkpoint; wenzelm parents: 7046 diff changeset	39
9204 e865dda0313e tuned rail setup; wenzelm parents: 8896 diff changeset	40	\railterm{percent,ppercent,underscore,lbrace,rbrace,atsign}
7167 0b2e3ef1d8f4 tuned; wenzelm parents: 7135 diff changeset	41	\railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
8596 b2ef22670f25 tuned; wenzelm parents: 8594 diff changeset	42	\railterm{name,nameref,text,type,term,prop,atom}
7134 320b412e5800 more stuff; wenzelm parents: 7050 diff changeset	43
13048 8b2eb3b78cc3 tuned; wenzelm parents: 12879 diff changeset	44	\railalias{ident}{\railtok{ident}}
8b2eb3b78cc3 tuned; wenzelm parents: 12879 diff changeset	45	\railalias{longident}{\railtok{longident}}
8b2eb3b78cc3 tuned; wenzelm parents: 12879 diff changeset	46	\railalias{symident}{\railtok{symident}}
8b2eb3b78cc3 tuned; wenzelm parents: 12879 diff changeset	47	\railalias{var}{\railtok{var}}
8b2eb3b78cc3 tuned; wenzelm parents: 12879 diff changeset	48	\railalias{textvar}{\railtok{textvar}}
8b2eb3b78cc3 tuned; wenzelm parents: 12879 diff changeset	49	\railalias{typefree}{\railtok{typefree}}
8b2eb3b78cc3 tuned; wenzelm parents: 12879 diff changeset	50	\railalias{typevar}{\railtok{typevar}}
8b2eb3b78cc3 tuned; wenzelm parents: 12879 diff changeset	51	\railalias{nat}{\railtok{nat}}
8b2eb3b78cc3 tuned; wenzelm parents: 12879 diff changeset	52	\railalias{string}{\railtok{string}}
8b2eb3b78cc3 tuned; wenzelm parents: 12879 diff changeset	53	\railalias{verbatim}{\railtok{verbatim}}
8b2eb3b78cc3 tuned; wenzelm parents: 12879 diff changeset	54	\railalias{keyword}{\railtok{keyword}}
8594 d2e2a3df6871 rail token vs. terminal; wenzelm parents: 8547 diff changeset	55
13048 8b2eb3b78cc3 tuned; wenzelm parents: 12879 diff changeset	56	\railalias{name}{\railqtok{name}}
8b2eb3b78cc3 tuned; wenzelm parents: 12879 diff changeset	57	\railalias{nameref}{\railqtok{nameref}}
8b2eb3b78cc3 tuned; wenzelm parents: 12879 diff changeset	58	\railalias{text}{\railqtok{text}}
8b2eb3b78cc3 tuned; wenzelm parents: 12879 diff changeset	59	\railalias{type}{\railqtok{type}}
8b2eb3b78cc3 tuned; wenzelm parents: 12879 diff changeset	60	\railalias{term}{\railqtok{term}}
8b2eb3b78cc3 tuned; wenzelm parents: 12879 diff changeset	61	\railalias{prop}{\railqtok{prop}}
8b2eb3b78cc3 tuned; wenzelm parents: 12879 diff changeset	62	\railalias{atom}{\railqtok{atom}}
7134 320b412e5800 more stuff; wenzelm parents: 7050 diff changeset	63
26786 e4e5d911e01c moved some railaliases here -- for proper scoping; wenzelm parents: 26782 diff changeset	64	\railalias{subseteq}{\isasymsubseteq}\railterm{subseteq}
e4e5d911e01c moved some railaliases here -- for proper scoping; wenzelm parents: 26782 diff changeset	65	\railalias{equiv}{\isasymequiv}\railterm{equiv}
e4e5d911e01c moved some railaliases here -- for proper scoping; wenzelm parents: 26782 diff changeset	66	\railalias{rightleftharpoons}{\isasymrightleftharpoons}\railterm{rightleftharpoons}
e4e5d911e01c moved some railaliases here -- for proper scoping; wenzelm parents: 26782 diff changeset	67	\railalias{rightharpoonup}{\isasymrightharpoonup}\railterm{rightharpoonup}
e4e5d911e01c moved some railaliases here -- for proper scoping; wenzelm parents: 26782 diff changeset	68	\railalias{leftharpoondown}{\isasymleftharpoondown}\railterm{leftharpoondown}
26848 d3d750ada604 added rail setup for verblbrace, verbrbrace; wenzelm parents: 26846 diff changeset	69	\railalias{verblbrace}{\texttt{\ttlbrace*}}\railterm{verblbrace}
d3d750ada604 added rail setup for verblbrace, verbrbrace; wenzelm parents: 26846 diff changeset	70	\railalias{verbrbrace}{\texttt{*\ttrbrace}}\railterm{verbrbrace}
d3d750ada604 added rail setup for verblbrace, verbrbrace; wenzelm parents: 26846 diff changeset	71
26786 e4e5d911e01c moved some railaliases here -- for proper scoping; wenzelm parents: 26782 diff changeset	72
18021 99d170aebb6e literal facts; wenzelm parents: 13048 diff changeset	73	\chardef\charbackquote=`\`
99d170aebb6e literal facts; wenzelm parents: 13048 diff changeset	74	\newcommand{\backquote}{\mbox{\tt\charbackquote}}
99d170aebb6e literal facts; wenzelm parents: 13048 diff changeset	75
7046 9f755ff43cff skeleton only; wenzelm parents: diff changeset	76
9f755ff43cff skeleton only; wenzelm parents: diff changeset	77	\begin{document}
9f755ff43cff skeleton only; wenzelm parents: diff changeset	78
9f755ff43cff skeleton only; wenzelm parents: diff changeset	79	\maketitle
9f755ff43cff skeleton only; wenzelm parents: diff changeset	80
9f755ff43cff skeleton only; wenzelm parents: diff changeset	81	\pagenumbering{roman} \tableofcontents \clearfirst
9f755ff43cff skeleton only; wenzelm parents: diff changeset	82
29718 cf48beb23a70 added parts; wenzelm parents: 29716 diff changeset	83	\part{Basic Concepts}
27035 d038a2ba87f6 renamed theory "intro" to "Introduction"; wenzelm parents: 26906 diff changeset	84	\input{Thy/document/Introduction.tex}
29716 b6266c4c68fe basic setup for chapter "The Isabelle/Isar Framework"; wenzelm parents: 28838 diff changeset	85	\input{Thy/document/Framework.tex}
29730 924c1fd5f303 added example "First-Order Logic" -- mostly from Trybulec Festschrift; wenzelm parents: 29718 diff changeset	86	\input{Thy/document/First_Order_Logic.tex}
29718 cf48beb23a70 added parts; wenzelm parents: 29716 diff changeset	87	\part{General Language Elements}
27037 33d95687514e renamed theory "syntax" to "Outer_Syntax"; wenzelm parents: 27035 diff changeset	88	\input{Thy/document/Outer_Syntax.tex}
28751 aad88e7344f0 moved section "Document preparation" to front; wenzelm parents: 27048 diff changeset	89	\input{Thy/document/Document_Preparation.tex}
26869 3bc332135aa7 added chapters for "Specifications" and "Proofs"; wenzelm parents: 26862 diff changeset	90	\input{Thy/document/Spec.tex}
3bc332135aa7 added chapters for "Specifications" and "Proofs"; wenzelm parents: 26862 diff changeset	91	\input{Thy/document/Proof.tex}
28762 f5d79aeffd81 separate chapter "Inner syntax --- the term language"; wenzelm parents: 28751 diff changeset	92	\input{Thy/document/Inner_Syntax.tex}
27048 0e86aab627f3 removed onsolete pure.thy (cf. Misc.thy); wenzelm parents: 27038 diff changeset	93	\input{Thy/document/Misc.tex}
26782 19363c70b5c4 converted generic.tex to Thy/Generic.thy; wenzelm parents: 26779 diff changeset	94	\input{Thy/document/Generic.tex}
29718 cf48beb23a70 added parts; wenzelm parents: 29716 diff changeset	95	\part{Object-Logics}
26840 ec46381f149d added logic-specific sessions; wenzelm parents: 26786 diff changeset	96	\input{Thy/document/HOL_Specific.tex}
ec46381f149d added logic-specific sessions; wenzelm parents: 26786 diff changeset	97	\input{Thy/document/HOLCF_Specific.tex}
ec46381f149d added logic-specific sessions; wenzelm parents: 26786 diff changeset	98	\input{Thy/document/ZF_Specific.tex}
7046 9f755ff43cff skeleton only; wenzelm parents: diff changeset	99
29718 cf48beb23a70 added parts; wenzelm parents: 29716 diff changeset	100	\part{Appendix}
7895 7c492d8bc8e3 updated; wenzelm parents: 7836 diff changeset	101	\appendix
26779 35809287ab23 converted refcard.tex to Thy/Quick_Reference.thy; wenzelm parents: 26767 diff changeset	102	\input{Thy/document/Quick_Reference.tex}
28838 d5db6dfcb34a moved table of standard Isabelle symbols to isar-ref manual; wenzelm parents: 28773 diff changeset	103	\let\int\intorig
d5db6dfcb34a moved table of standard Isabelle symbols to isar-ref manual; wenzelm parents: 28773 diff changeset	104	\input{Thy/document/Symbols.tex}
26846 2e6726015771 removed obsolete conversion guide -- converted only section on tactics; wenzelm parents: 26840 diff changeset	105	\input{Thy/document/ML_Tactic.tex}
7895 7c492d8bc8e3 updated; wenzelm parents: 7836 diff changeset	106
7046 9f755ff43cff skeleton only; wenzelm parents: diff changeset	107	\begingroup
30116 1fb1833cb199 \bibliographystyle{abbrv} for newer ref manuals; wenzelm parents: 29730 diff changeset	108	\bibliographystyle{abbrv} \small\raggedright\frenchspacing
7046 9f755ff43cff skeleton only; wenzelm parents: diff changeset	109	\bibliography{../manual}
9f755ff43cff skeleton only; wenzelm parents: diff changeset	110	\endgroup
9f755ff43cff skeleton only; wenzelm parents: diff changeset	111
8828 5be2d1745c61 improved indexing; wenzelm parents: 8596 diff changeset	112	\printindex
7046 9f755ff43cff skeleton only; wenzelm parents: diff changeset	113
9f755ff43cff skeleton only; wenzelm parents: diff changeset	114	\end{document}

author	haftmann
	Sat, 13 Jun 2009 16:32:38 +0200
changeset 31626	fe35b72b9ef0
parent 30569	696f93184f0d
child 40893	7d88ebdce380
permissions	-rw-r--r--