We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 7db4cd4 commit 95a8c4dCopy full SHA for 95a8c4d
.gitignore
@@ -18,3 +18,4 @@ metamath.exe
18
*.mmp
19
*.mmt
20
*.mms
21
+*.html
scripts/minimize
@@ -4,7 +4,8 @@
4
theorem="$1"
5
source="${2:-set.mm}"
6
7
-metamath "read ${source}" \
+metamath "SET UNIFICATION_TIMEOUT 1000000"\
8
+ "read ${source}" \
9
"prove ${theorem}" \
10
'minimize */allow */no_new ax-*' \
11
'save new /compressed' \
scripts/regen-discouraged
@@ -5,7 +5,7 @@
# We sort "show discouraged" results to ignore benign reordering, and sort
# using LC_ALL=C so that the current locale won't affect the reorder.
-result_file='discouraged'
+result_file='discouraged1'
while [ $# -gt 0 ] ; do
case "$1" in
0 commit comments