File tree Expand file tree Collapse file tree 5 files changed +5
-13
lines changed
Expand file tree Collapse file tree 5 files changed +5
-13
lines changed Original file line number Diff line number Diff line change 11# Attributes
22
3- Mathlib version: ` 85c6303552add8dfd66879105baf43ba557f4be7 `
3+ Mathlib version: ` a492302f08689dc5487dc81f7f9726572b35315c `
44
55## Std.Internal.tree_tac
66 simp theorems used by internal DTreeMap lemmas
@@ -741,14 +741,6 @@ Register an Expr presenter. It must have the type `ProofWidgets.ExprPresenter`.
741741## extern
742742 builtin and foreign functions
743743
744- ## field_simps
745- The simpset `field_simps` is used by the tactic `field_simp` to
746- reduce an expression in a field to an expression of the form `n / d` where `n` and `d` are
747- division-free.
748-
749- ## field_simps_proc
750- simproc set for field_simps_proc
751-
752744## fin_omega
753745 A simp set for the `fin_omega` wrapper around `omega`.
754746
Original file line number Diff line number Diff line change 11# Commands
22
3- Mathlib version: ` 85c6303552add8dfd66879105baf43ba557f4be7 `
3+ Mathlib version: ` a492302f08689dc5487dc81f7f9726572b35315c `
44
55## \# adaptation_note
66Defined in: ` adaptationNoteCmd `
Original file line number Diff line number Diff line change 11# Options
22
3- Mathlib version: ` 85c6303552add8dfd66879105baf43ba557f4be7 `
3+ Mathlib version: ` a492302f08689dc5487dc81f7f9726572b35315c `
44
55## Elab.async
66type: ` Bool `
Original file line number Diff line number Diff line change 11# Tactics
22
3- Mathlib version: ` 85c6303552add8dfd66879105baf43ba557f4be7 `
3+ Mathlib version: ` a492302f08689dc5487dc81f7f9726572b35315c `
44
55## \# adaptation_note
66Defined in: ` «tactic#adaptation_note_» `
Original file line number Diff line number Diff line change 55 "type" : " git" ,
66 "subDir" : null ,
77 "scope" : " " ,
8- "rev" : " 85c6303552add8dfd66879105baf43ba557f4be7 " ,
8+ "rev" : " a492302f08689dc5487dc81f7f9726572b35315c " ,
99 "name" : " mathlib" ,
1010 "manifestFile" : " lake-manifest.json" ,
1111 "inputRev" : " master" ,
You can’t perform that action at this time.
0 commit comments