# HG changeset patch # User ballarin # Date 1190134435 -7200 # Node ID 7865c239ba081a94e9df25f2b4c19183a85eb9e9 # Parent 448edc627ee43270450c7981c3063ba5c8329911 New diagnostic command print_orders. diff -r 448edc627ee4 -r 7865c239ba08 etc/isar-keywords-HOL-Nominal.el --- a/etc/isar-keywords-HOL-Nominal.el Tue Sep 18 18:53:12 2007 +0200 +++ b/etc/isar-keywords-HOL-Nominal.el Tue Sep 18 18:53:55 2007 +0200 @@ -156,6 +156,7 @@ "print_locales" "print_methods" "print_noatp_rules" + "print_orders" "print_rules" "print_simpset" "print_statement" @@ -336,6 +337,7 @@ "print_locales" "print_methods" "print_noatp_rules" + "print_orders" "print_rules" "print_simpset" "print_statement" diff -r 448edc627ee4 -r 7865c239ba08 etc/isar-keywords.el --- a/etc/isar-keywords.el Tue Sep 18 18:53:12 2007 +0200 +++ b/etc/isar-keywords.el Tue Sep 18 18:53:55 2007 +0200 @@ -157,6 +157,7 @@ "print_locales" "print_methods" "print_noatp_rules" + "print_orders" "print_rules" "print_simpset" "print_statement" @@ -351,6 +352,7 @@ "print_locales" "print_methods" "print_noatp_rules" + "print_orders" "print_rules" "print_simpset" "print_statement"