add proof method "order" to command "try0"

--- a/NEWS	Sat Jul 01 16:47:52 2023 +0200
+++ b/NEWS	Sun Jul 02 14:28:20 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.
 

--- a/src/HOL/Tools/try0.ML	Sat Jul 01 16:47:52 2023 +0200
+++ b/src/HOL/Tools/try0.ML	Sun Jul 02 14:28:20 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;