# HG changeset patch
# User wenzelm
# Date 1364651826 -3600
# Node ID fcd5af4aac2b5592dad4e29fea9ca51e5e7b3004
# Parent  98029ceda8ce79c9a886652a5449b1dd4e4be4ff
added 'print_defn_rules' command;
tuned;

diff -r 98029ceda8ce -r fcd5af4aac2b etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Sat Mar 30 13:40:19 2013 +0100
+++ b/etc/isar-keywords-ZF.el	Sat Mar 30 14:57:06 2013 +0100
@@ -132,6 +132,7 @@
     "print_commands"
     "print_configs"
     "print_context"
+    "print_defn_rules"
     "print_dependencies"
     "print_drafts"
     "print_facts"
@@ -300,6 +301,7 @@
     "print_commands"
     "print_configs"
     "print_context"
+    "print_defn_rules"
     "print_dependencies"
     "print_drafts"
     "print_facts"
diff -r 98029ceda8ce -r fcd5af4aac2b etc/isar-keywords.el
--- a/etc/isar-keywords.el	Sat Mar 30 13:40:19 2013 +0100
+++ b/etc/isar-keywords.el	Sat Mar 30 14:57:06 2013 +0100
@@ -185,6 +185,7 @@
     "print_commands"
     "print_configs"
     "print_context"
+    "print_defn_rules"
     "print_dependencies"
     "print_drafts"
     "print_facts"
@@ -407,6 +408,7 @@
     "print_commands"
     "print_configs"
     "print_context"
+    "print_defn_rules"
     "print_dependencies"
     "print_drafts"
     "print_facts"
diff -r 98029ceda8ce -r fcd5af4aac2b src/Doc/IsarRef/Spec.thy
--- a/src/Doc/IsarRef/Spec.thy	Sat Mar 30 13:40:19 2013 +0100
+++ b/src/Doc/IsarRef/Spec.thy	Sat Mar 30 14:57:06 2013 +0100
@@ -264,6 +264,7 @@
     @{command_def "axiomatization"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
     @{command_def "definition"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{attribute_def "defn"} & : & @{text attribute} \\
+    @{command_def "print_defn_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\
     @{command_def "abbreviation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "print_abbrevs"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\
   \end{matharray}
@@ -317,7 +318,10 @@
   well as additional conditions, e.g.\ @{text "f x y = t"} instead of
   @{text "f \<equiv> \<lambda>x y. t"} and @{text "y \<noteq> 0 \<Longrightarrow> g x y = u"} instead of an
   unrestricted @{text "g \<equiv> \<lambda>x y. u"}.
-  
+
+  \item @{command "print_defn_rules"} prints the definitional rewrite rules
+  declared via @{attribute defn} in the current context.
+
   \item @{command "abbreviation"}~@{text "c \<WHERE> eq"} introduces a
   syntactic constant which is associated with a certain term according
   to the meta-level equality @{text eq}.
diff -r 98029ceda8ce -r fcd5af4aac2b src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Mar 30 13:40:19 2013 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sat Mar 30 14:57:06 2013 +0100
@@ -781,8 +781,14 @@
       Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
 
 val _ =
+  Outer_Syntax.improper_command @{command_spec "print_defn_rules"}
+    "print definitional rewrite rules of context"
+    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+      Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of)));
+
+val _ =
   Outer_Syntax.improper_command @{command_spec "print_abbrevs"}
-    "print constant abbreviation of context"
+    "print constant abbreviations of context"
     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
       Toplevel.keep (Proof_Context.print_abbrevs o Toplevel.context_of)));
 
diff -r 98029ceda8ce -r fcd5af4aac2b src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Sat Mar 30 13:40:19 2013 +0100
+++ b/src/Pure/Isar/local_defs.ML	Sat Mar 30 14:57:06 2013 +0100
@@ -169,7 +169,7 @@
 
 (** defived definitions **)
 
-(* transformation rules *)
+(* transformation via rewrite rules *)
 
 structure Rules = Generic_Data
 (
@@ -180,7 +180,7 @@
 );
 
 fun print_rules ctxt =
-  Pretty.writeln (Pretty.big_list "definitional transformations:"
+  Pretty.writeln (Pretty.big_list "definitional rewrite rules:"
     (map (Display.pretty_thm_item ctxt) (Rules.get (Context.Proof ctxt))));
 
 val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm);
diff -r 98029ceda8ce -r fcd5af4aac2b src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sat Mar 30 13:40:19 2013 +0100
+++ b/src/Pure/Pure.thy	Sat Mar 30 14:57:06 2013 +0100
@@ -75,7 +75,7 @@
   and "back" :: prf_script % "proof"
   and "Isabelle.command" :: control
   and "help" "print_commands" "print_configs"
-    "print_context" "print_theory" "print_syntax" "print_abbrevs"
+    "print_context" "print_theory" "print_syntax" "print_abbrevs" "print_defn_rules"
     "print_theorems" "print_locales" "print_classes" "print_locale"
     "print_interps" "print_dependencies" "print_attributes"
     "print_simpset" "print_rules" "print_trans_rules" "print_methods"