# HG changeset patch
# User wenzelm
# Date 1688323267 -7200
# Node ID d4125fc10c0c2ef42494a2197a6cf689873b8b50
# Parent  4fe65149f3fd642c278dc55b61f3e69805916981# Parent  76dd9b9cf62460be701e19b41d89b29d80c2e8d5
merged

diff -r 76dd9b9cf624 -r d4125fc10c0c NEWS
--- a/NEWS	Sun Jul 02 20:09:12 2023 +0200
+++ b/NEWS	Sun Jul 02 20:41:07 2023 +0200
@@ -76,6 +76,9 @@
   - Made clausifier more robust in the face of nested lambdas.
     Minor INCOMPATIBILITY.
 
+* Command "try0":
+  - Add proof method "order".
+
 * 'primcorec': Made the internal tactic more robust in the face of
   nested corecursion.
 
diff -r 76dd9b9cf624 -r d4125fc10c0c src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Sun Jul 02 20:09:12 2023 +0200
+++ b/src/HOL/Tools/try0.ML	Sun Jul 02 20:41:07 2023 +0200
@@ -93,7 +93,8 @@
    ("fastforce", ((false, false), full_attrs)),
    ("force", ((false, false), full_attrs)),
    ("meson", ((false, false), metis_attrs)),
-   ("satx", ((false, false), no_attrs))];
+   ("satx", ((false, false), no_attrs)),
+   ("order", ((false, true), no_attrs))];
 
 val apply_methods = map apply_named_method named_methods;