--- a/src/Doc/Isar_Ref/Generic.thy Wed Jun 06 13:04:52 2018 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy Wed Jun 06 18:19:55 2018 +0200
@@ -275,8 +275,9 @@
opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')'
;
- @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'split' (() | '!' | 'del') |
- 'cong' (() | 'add' | 'del')) ':' @{syntax thms}
+ @{syntax_def simpmod}: ('add' | 'del' | 'flip' | 'only' |
+ 'split' (() | '!' | 'del') | 'cong' (() | 'add' | 'del'))
+ ':' @{syntax thms}
\<close>}
\<^descr> @{method simp} invokes the Simplifier on the first subgoal, after
@@ -292,6 +293,11 @@
situations to perform the intended simplification step!
\<^medskip>
+Modifier \<open>flip\<close> deletes the following theorems from the simpset and adds
+their symmetric version (i.e.\ lhs and rhs exchanged). No warning is shown
+if the original theorem was not present.
+
+ \<^medskip>
The \<open>only\<close> modifier first removes all other rewrite rules, looper tactics
(including split rules), congruence rules, and then behaves like \<open>add\<close>.
Implicit solvers remain, which means that trivial rules like reflexivity or