equal
deleted
inserted
replaced
356 \texttt{Asm_full_simp_tac 1} & & simp \\ |
356 \texttt{Asm_full_simp_tac 1} & & simp \\ |
357 \texttt{ALLGOALS Asm_full_simp_tac} & & simp_all \\[0.5ex] |
357 \texttt{ALLGOALS Asm_full_simp_tac} & & simp_all \\[0.5ex] |
358 \texttt{Simp_tac 1} & & simp~(no_asm) \\ |
358 \texttt{Simp_tac 1} & & simp~(no_asm) \\ |
359 \texttt{Asm_simp_tac 1} & & simp~(no_asm_simp) \\ |
359 \texttt{Asm_simp_tac 1} & & simp~(no_asm_simp) \\ |
360 \texttt{Full_simp_tac 1} & & simp~(no_asm_use) \\ |
360 \texttt{Full_simp_tac 1} & & simp~(no_asm_use) \\ |
|
361 \texttt{Asm_lr_simp_tac 1} & & simp~(asm_lr) \\ |
361 \end{matharray} |
362 \end{matharray} |
362 |
363 |
363 Isar also provides separate method modifier syntax for augmenting the |
364 Isar also provides separate method modifier syntax for augmenting the |
364 Simplifier context (see \S\ref{sec:simplifier}), which is known as the |
365 Simplifier context (see \S\ref{sec:simplifier}), which is known as the |
365 ``simpset'' in ML. A typical ML expression with simpset changes looks like |
366 ``simpset'' in ML. A typical ML expression with simpset changes looks like |