# HG changeset patch # User wenzelm # Date 1474054519 -7200 # Node ID f83ef97d8d7d8f28260dfb1a45efd047c4018845 # Parent 4ce989e962e0749a402491d8378c05d08f8316df more symbols -- as in the printed document; diff -r 4ce989e962e0 -r f83ef97d8d7d src/Doc/Main/Main_Doc.thy --- a/src/Doc/Main/Main_Doc.thy Fri Sep 16 21:28:09 2016 +0200 +++ b/src/Doc/Main/Main_Doc.thy Fri Sep 16 21:35:19 2016 +0200 @@ -31,7 +31,9 @@ \section*{HOL} -The basic logic: @{prop "x = y"}, @{const True}, @{const False}, @{prop"Not P"}, @{prop"P & Q"}, @{prop "P | Q"}, @{prop "P --> Q"}, @{prop"ALL x. P"}, @{prop"EX x. P"}, @{prop"EX! x. P"}, @{term"THE x. P"}. +The basic logic: @{prop "x = y"}, @{const True}, @{const False}, @{prop "\ P"}, @{prop"P \ Q"}, +@{prop "P \ Q"}, @{prop "P \ Q"}, @{prop "\x. P"}, @{prop "\x. P"}, @{prop"\! x. P"}, +@{term"THE x. P"}. \<^smallskip> \begin{tabular}{@ {} l @ {~::~} l @ {}} @@ -42,10 +44,10 @@ \subsubsection*{Syntax} \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} -@{term"~(x = y)"} & @{term[source]"\ (x = y)"} & (\<^verbatim>\~=\)\\ +@{term"\ (x = y)"} & @{term[source]"\ (x = y)"} & (\<^verbatim>\~=\)\\ @{term[source]"P \ Q"} & @{term"P \ Q"} \\ @{term"If x y z"} & @{term[source]"If x y z"}\\ -@{term"Let e\<^sub>1 (%x. e\<^sub>2)"} & @{term[source]"Let e\<^sub>1 (\x. e\<^sub>2)"}\\ +@{term"Let e\<^sub>1 (\x. e\<^sub>2)"} & @{term[source]"Let e\<^sub>1 (\x. e\<^sub>2)"}\\ \end{supertabular} @@ -72,10 +74,10 @@ \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} @{term[source]"x \ y"} & @{term"x \ y"} & (\<^verbatim>\>=\)\\ @{term[source]"x > y"} & @{term"x > y"}\\ -@{term"ALL x<=y. P"} & @{term[source]"\x. x \ y \ P"}\\ -@{term"EX x<=y. P"} & @{term[source]"\x. x \ y \ P"}\\ +@{term "\x\y. P"} & @{term[source]"\x. x \ y \ P"}\\ +@{term "\x\y. P"} & @{term[source]"\x. x \ y \ P"}\\ \multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\ -@{term"LEAST x. P"} & @{term[source]"Least (\x. P)"}\\ +@{term "LEAST x. P"} & @{term[source]"Least (\x. P)"}\\ \end{supertabular} @@ -131,20 +133,20 @@ \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} \{a\<^sub>1,\,a\<^sub>n}\ & \insert a\<^sub>1 (\ (insert a\<^sub>n {})\)\\\ -@{term"a ~: A"} & @{term[source]"\(x \ A)"}\\ -@{term"A \ B"} & @{term[source]"A \ B"}\\ -@{term"A \ B"} & @{term[source]"A < B"}\\ +@{term "a \ A"} & @{term[source]"\(x \ A)"}\\ +@{term "A \ B"} & @{term[source]"A \ B"}\\ +@{term "A \ B"} & @{term[source]"A < B"}\\ @{term[source]"A \ B"} & @{term[source]"B \ A"}\\ @{term[source]"A \ B"} & @{term[source]"B < A"}\\ -@{term"{x. P}"} & @{term[source]"Collect (\x. P)"}\\ +@{term "{x. P}"} & @{term[source]"Collect (\x. P)"}\\ \{t | x\<^sub>1 \ x\<^sub>n. P}\ & \{v. \x\<^sub>1 \ x\<^sub>n. v = t \ P}\\\ @{term[source]"\x\I. A"} & @{term[source]"UNION I (\x. A)"} & (\texttt{UN})\\ @{term[source]"\x. A"} & @{term[source]"UNION UNIV (\x. A)"}\\ @{term[source]"\x\I. A"} & @{term[source]"INTER I (\x. A)"} & (\texttt{INT})\\ @{term[source]"\x. A"} & @{term[source]"INTER UNIV (\x. A)"}\\ -@{term"ALL x:A. P"} & @{term[source]"Ball A (\x. P)"}\\ -@{term"EX x:A. P"} & @{term[source]"Bex A (\x. P)"}\\ -@{term"range f"} & @{term[source]"f ` UNIV"}\\ +@{term "\x\A. P"} & @{term[source]"Ball A (\x. P)"}\\ +@{term "\x\A. P"} & @{term[source]"Bex A (\x. P)"}\\ +@{term "range f"} & @{term[source]"f ` UNIV"}\\ \end{supertabular} @@ -225,15 +227,15 @@ \subsubsection*{Syntax} \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}} -@{term"Pair a b"} & @{term[source]"Pair a b"}\\ -@{term"case_prod (\x y. t)"} & @{term[source]"case_prod (\x y. t)"}\\ -@{term"A \ B"} & \Sigma A (\\<^raw:\_>. B)\ +@{term "Pair a b"} & @{term[source]"Pair a b"}\\ +@{term "case_prod (\x y. t)"} & @{term[source]"case_prod (\x y. t)"}\\ +@{term "A \ B"} & \Sigma A (\\<^raw:\_>. B)\ \end{tabular} Pairs may be nested. Nesting to the right is printed as a tuple, -e.g.\ \mbox{@{term"(a,b,c)"}} is really \mbox{\(a, (b, c))\.} +e.g.\ \mbox{@{term "(a,b,c)"}} is really \mbox{\(a, (b, c))\.} Pattern matching with pairs and tuples extends to all binders, -e.g.\ \mbox{@{prop"ALL (x,y):A. P"},} @{term"{(x,y). P}"}, etc. +e.g.\ \mbox{@{prop "\(x,y)\A. P"},} @{term "{(x,y). P}"}, etc. \section*{Relation} @@ -331,7 +333,7 @@ \subsubsection*{Syntax} \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} -@{term"abs x"} & @{term[source]"abs x"} +@{term "\x\"} & @{term[source] "abs x"} \end{tabular} @@ -404,19 +406,19 @@ \begin{supertabular}{@ {} l @ {~::~} l @ {}} @{const Finite_Set.finite} & @{term_type_only Finite_Set.finite "'a set\bool"}\\ -@{const Finite_Set.card} & @{term_type_only Finite_Set.card "'a set => nat"}\\ +@{const Finite_Set.card} & @{term_type_only Finite_Set.card "'a set \ nat"}\\ @{const Finite_Set.fold} & @{term_type_only Finite_Set.fold "('a \ 'b \ 'b) \ 'b \ 'a set \ 'b"}\\ -@{const Groups_Big.setsum} & @{term_type_only Groups_Big.setsum "('a => 'b) => 'a set => 'b::comm_monoid_add"}\\ -@{const Groups_Big.setprod} & @{term_type_only Groups_Big.setprod "('a => 'b) => 'a set => 'b::comm_monoid_mult"}\\ +@{const Groups_Big.setsum} & @{term_type_only Groups_Big.setsum "('a \ 'b) \ 'a set \ 'b::comm_monoid_add"}\\ +@{const Groups_Big.setprod} & @{term_type_only Groups_Big.setprod "('a \ 'b) \ 'a set \ 'b::comm_monoid_mult"}\\ \end{supertabular} \subsubsection*{Syntax} \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}} -@{term"setsum (%x. x) A"} & @{term[source]"setsum (\x. x) A"} & (\<^verbatim>\SUM\)\\ -@{term"setsum (%x. t) A"} & @{term[source]"setsum (\x. t) A"}\\ -@{term[source]"\x|P. t"} & @{term"\x|P. t"}\\ +@{term "setsum (\x. x) A"} & @{term[source]"setsum (\x. x) A"} & (\<^verbatim>\SUM\)\\ +@{term "setsum (\x. t) A"} & @{term[source]"setsum (\x. t) A"}\\ +@{term[source] "\x|P. t"} & @{term"\x|P. t"}\\ \multicolumn{2}{@ {}l@ {}}{Similarly for \\\ instead of \\\} & (\<^verbatim>\PROD\)\\ \end{supertabular} @@ -461,10 +463,10 @@ @{term[source] "\i\n. A"} & @{term[source] "\i \ {..n}. A"}\\ @{term[source] "\ii \ {..\\ instead of \\\}\\ -@{term "setsum (%x. t) {a..b}"} & @{term[source] "setsum (\x. t) {a..b}"}\\ -@{term "setsum (%x. t) {a..x. t) {a..x. t) {..b}"}\\ -@{term "setsum (%x. t) {..x. t) {..x. t) {a..b}"} & @{term[source] "setsum (\x. t) {a..b}"}\\ +@{term "setsum (\x. t) {a..x. t) {a..x. t) {..b}"} & @{term[source] "setsum (\x. t) {..b}"}\\ +@{term "setsum (\x. t) {..x. t) {..\\ instead of \\\}\\ \end{supertabular}