diff options
| author | thery | 2019-01-21 18:40:54 +0100 |
|---|---|---|
| committer | thery | 2019-01-21 18:40:54 +0100 |
| commit | 3dcf2f79d422f671aadf441c5318994c9cfea6be (patch) | |
| tree | 8ae0c631e1ada98a148555acc137b35811897649 | |
| parent | b8da6225e3867408f5d1ad0c716618c4228a1ad2 (diff) | |
ring and field simplify can take no arguments
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 59602581c7..554bfefa0a 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -4343,7 +4343,7 @@ Automating distributivity, constant propagation) and comparing syntactically the results. -.. tacn:: ring_simplify {+ @term} +.. tacn:: ring_simplify {* @term} :name: ring_simplify This tactic applies the normalization procedure described above to @@ -4357,7 +4357,7 @@ the tactic and how to declare new ring structures. All declared field structures can be printed with the ``Print Rings`` command. .. tacn:: field - field_simplify {+ @term} + field_simplify {* @term} field_simplify_eq :name: field; field_simplify; field_simplify_eq |