doc-src/Tutorial/tutorial.ind

Arithmetic.

\begin{theindex}

  \item {\tt[]}, \bold{7}
  \item {\tt\#}, \bold{7}
  \item {\ttnot}, \bold{3}
  \item {\tt-->}, \bold{3}
  \item {\tt\&}, \bold{3}
  \item {\ttor}, \bold{3}
  \item {\tt?}, \bold{3}, 4
  \item {\ttall}, \bold{3}
  \item {\ttuniquex}, \bold{3}
  \item {\tt *}, \bold{17}
  \item {\tt +}, \bold{17}
  \item {\tt -}, \bold{17, 18}
  \item {\tt <}, \bold{17}
  \item {\tt <=}, \bold{17}
  \item \ttlbr, \bold{9}
  \item \ttrbr, \bold{9}
  \item {\tt==>}, \bold{9}
  \item {\tt==}, \bold{19}
  \item {\tt\%}, \bold{3}
  \item {\tt =>}, \bold{2}

  \indexspace

  \item {\tt addsimps}, \bold{22}
  \item {\tt Addsplits}, \bold{24}
  \item {\tt addsplits}, \bold{24}
  \item {\tt and}, \bold{29}
  \item {\tt arith_tac}, \bold{17}
  \item arithmetic, 17--18, 24
  \item {\tt Asm_full_simp_tac}, \bold{21}
  \item {\tt asm_full_simp_tac}, \bold{22}
  \item {\tt Asm_simp_tac}, \bold{21}
  \item {\tt asm_simp_tac}, \bold{22}

  \indexspace

  \item {\tt bool}, 2

  \indexspace

  \item {\tt case}, \bold{3}, 4, \bold{13}, 24
  \item {\tt constdefs}, \bold{19}
  \item {\tt consts}, \bold{7}
  \item {\tt context}, \bold{11}
  \item current theory, \bold{11}

  \indexspace

  \item {\tt datatype}, \bold{7}, 29--33
  \item {\tt defs}, \bold{19}
  \item {\tt delsimps}, \bold{22}
  \item {\tt Delsplits}, \bold{24}
  \item {\tt delsplits}, \bold{24}
  \item {\tt div}, \bold{17}

  \indexspace

  \item {\tt exhaust_tac}, \bold{14}

  \indexspace

  \item {\tt False}, \bold{3}
  \item formula, \bold{3}
  \item {\tt Full_simp_tac}, \bold{21}
  \item {\tt full_simp_tac}, \bold{22}

  \indexspace

  \item {\tt hd}, \bold{12}

  \indexspace

  \item {\tt if}, \bold{3}, 4, 24
  \item {\tt infixr}, \bold{7}
  \item inner syntax, \bold{8}

  \indexspace

  \item {\tt LEAST}, \bold{17}
  \item {\tt let}, \bold{3}, 4, 23
  \item {\tt list}, 2
  \item loading theories, 12

  \indexspace

  \item {\tt Main}, \bold{2}
  \item {\tt max}, \bold{17, 18}
  \item measure function, \bold{36}
  \item {\tt min}, \bold{17, 18}
  \item {\tt mod}, \bold{17}
  \item {\tt mutual_induct_tac}, \bold{30}

  \indexspace

  \item {\tt nat}, 2, \bold{17}
  \item {\tt None}, \bold{33}

  \indexspace

  \item {\tt option}, \bold{33}

  \indexspace

  \item parent theory, \bold{1}
  \item primitive recursion, \bold{13}
  \item {\tt primrec}, 7, \bold{13}, 29--33
  \item proof scripts, \bold{2}

  \indexspace

  \item {\tt recdef}, 35--38
  \item reloading theories, 12

  \indexspace

  \item schematic variable, \bold{4}
  \item {\tt set}, 2
  \item {\tt show_brackets}, \bold{4}
  \item {\tt show_types}, \bold{3}, 11
  \item {\tt Simp_tac}, \bold{21}
  \item {\tt simp_tac}, \bold{22}
  \item simplifier, \bold{20}
  \item simpset, \bold{21}
  \item {\tt Some}, \bold{33}

  \indexspace

  \item tactic, \bold{11}
  \item term, \bold{3}
  \item theory, \bold{1}
  \item {\tt tl}, \bold{12}
  \item total, \bold{7}
  \item tracing the simplifier, \bold{25}
  \item {\tt True}, \bold{3}
  \item type constraints, \bold{3}
  \item type inference, \bold{3}
  \item type synonyms, \bold{18}
  \item {\tt types}, \bold{18}

  \indexspace

  \item unknown, \bold{4}
  \item {\tt update_thy}, \bold{12}
  \item {\tt use_thy}, \bold{2}, 12

\end{theindex}