From cd568f32f898d20350e8689f76a19ea8a5f6b3f1 Mon Sep 17 00:00:00 2001 From: GitHub Action Date: Sun, 2 Jun 2024 08:02:26 +0000 Subject: [PATCH] generated by GitHub Action --- lake-manifest.json | 6 +++--- src/tactics.md | 8 -------- 2 files changed, 3 insertions(+), 11 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index a1eb283..8027550 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "rev": "60d622c124cebcecc000853cdae93f4251f4beb5", + "rev": "dfe82086e9904edfc04eb0f5205c85647956897d", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -22,7 +22,7 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "70ec1d99be1e1b835d831f39c01b0d14921d2118", + "rev": "d68b34fabd37681e6732be752b7e90aaac7aa0e0", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -58,7 +58,7 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "30a8ef8d300dbb0f18287dd8589dd86b61bc217a", + "rev": "6f758e582b2ad1cb121bf88aa1a178e284315af5", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", diff --git a/src/tactics.md b/src/tactics.md index 7058e2d..98e84e1 100644 --- a/src/tactics.md +++ b/src/tactics.md @@ -245,14 +245,6 @@ Defined in: `Aesop.BuiltinRules.tacticAesop_destruct_products` Defined in: `Aesop.BuiltinRules.tacticAesop_split_hyps` -# aesop_subst -Defined in: `Aesop.BuiltinRules.«tacticAesop_subst[_,,]»` - - -# aesop_subst -Defined in: `Aesop.BuiltinRules.tacticAesop_subst_` - - # aesop_unfold Defined in: `Aesop.«tacticAesop_unfold[_,,]»`