# 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 \ theory"} & (axiomatic!) \\ @{command_def "definition"} & : & @{text "local_theory \ local_theory"} \\ @{attribute_def "defn"} & : & @{text attribute} \\ + @{command_def "print_defn_rules"}@{text "\<^sup>*"} & : & @{text "context \ "} \\ @{command_def "abbreviation"} & : & @{text "local_theory \ local_theory"} \\ @{command_def "print_abbrevs"}@{text "\<^sup>*"} & : & @{text "context \ "} \\ \end{matharray} @@ -317,7 +318,10 @@ well as additional conditions, e.g.\ @{text "f x y = t"} instead of @{text "f \ \x y. t"} and @{text "y \ 0 \ g x y = u"} instead of an unrestricted @{text "g \ \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 \ 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"