doc-src/IsarOverview/Isar/document/session.tex
| author |
avigad |
|
Tue, 12 Jul 2005 17:56:03 +0200 |
| changeset 16775 |
c1b87ef4a1c3 |
| parent 13999 |
454a2ad0c381
|
| permissions |
-rw-r--r-- |
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
added lemmas to Ring_and_Field.thy (reasoning about signs, fractions, etc.)
renamed simplification rules for abs (abs_of_pos, etc.)
renamed rules for multiplication and signs (mult_pos_pos, etc.)
moved lemmas involving fractions from NatSimprocs.thy
added setsum_mono3 to FiniteSet.thy
added simplification rules for powers to Parity.thy
|
13999
|
1 |
\input{Logic.tex}
|
|
|
2 |
|
|
|
3 |
\input{Induction.tex}
|
|
|
4 |
|
|
|
5 |
%%% Local Variables:
|
|
|
6 |
%%% mode: latex
|
|
|
7 |
%%% TeX-master: "root"
|
|
|
8 |
%%% End:
|