# HG changeset patch
# User desharna
# Date 1688300900 -7200
# Node ID 4fe65149f3fd642c278dc55b61f3e69805916981
# Parent  8c0d3c879f7cc48515c22f88d2e2f9dbca3739d7
add proof method "order" to command "try0"

diff -r 8c0d3c879f7c -r 4fe65149f3fd NEWS
--- 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.
 
diff -r 8c0d3c879f7c -r 4fe65149f3fd src/HOL/Tools/try0.ML
--- 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;