added 'print_defn_rules' command;
authorwenzelm
Sat Mar 30 14:57:06 2013 +0100 (2013-03-30)
changeset 51585fcd5af4aac2b
parent 51584 98029ceda8ce
child 51586 7c59fe17f495
child 51587 7050c4656fd8
added 'print_defn_rules' command;
tuned;
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/Doc/IsarRef/Spec.thy
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/local_defs.ML
src/Pure/Pure.thy
     1.1 --- a/etc/isar-keywords-ZF.el	Sat Mar 30 13:40:19 2013 +0100
     1.2 +++ b/etc/isar-keywords-ZF.el	Sat Mar 30 14:57:06 2013 +0100
     1.3 @@ -132,6 +132,7 @@
     1.4      "print_commands"
     1.5      "print_configs"
     1.6      "print_context"
     1.7 +    "print_defn_rules"
     1.8      "print_dependencies"
     1.9      "print_drafts"
    1.10      "print_facts"
    1.11 @@ -300,6 +301,7 @@
    1.12      "print_commands"
    1.13      "print_configs"
    1.14      "print_context"
    1.15 +    "print_defn_rules"
    1.16      "print_dependencies"
    1.17      "print_drafts"
    1.18      "print_facts"
     2.1 --- a/etc/isar-keywords.el	Sat Mar 30 13:40:19 2013 +0100
     2.2 +++ b/etc/isar-keywords.el	Sat Mar 30 14:57:06 2013 +0100
     2.3 @@ -185,6 +185,7 @@
     2.4      "print_commands"
     2.5      "print_configs"
     2.6      "print_context"
     2.7 +    "print_defn_rules"
     2.8      "print_dependencies"
     2.9      "print_drafts"
    2.10      "print_facts"
    2.11 @@ -407,6 +408,7 @@
    2.12      "print_commands"
    2.13      "print_configs"
    2.14      "print_context"
    2.15 +    "print_defn_rules"
    2.16      "print_dependencies"
    2.17      "print_drafts"
    2.18      "print_facts"
     3.1 --- a/src/Doc/IsarRef/Spec.thy	Sat Mar 30 13:40:19 2013 +0100
     3.2 +++ b/src/Doc/IsarRef/Spec.thy	Sat Mar 30 14:57:06 2013 +0100
     3.3 @@ -264,6 +264,7 @@
     3.4      @{command_def "axiomatization"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
     3.5      @{command_def "definition"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     3.6      @{attribute_def "defn"} & : & @{text attribute} \\
     3.7 +    @{command_def "print_defn_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\
     3.8      @{command_def "abbreviation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     3.9      @{command_def "print_abbrevs"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\
    3.10    \end{matharray}
    3.11 @@ -317,7 +318,10 @@
    3.12    well as additional conditions, e.g.\ @{text "f x y = t"} instead of
    3.13    @{text "f \<equiv> \<lambda>x y. t"} and @{text "y \<noteq> 0 \<Longrightarrow> g x y = u"} instead of an
    3.14    unrestricted @{text "g \<equiv> \<lambda>x y. u"}.
    3.15 -  
    3.16 +
    3.17 +  \item @{command "print_defn_rules"} prints the definitional rewrite rules
    3.18 +  declared via @{attribute defn} in the current context.
    3.19 +
    3.20    \item @{command "abbreviation"}~@{text "c \<WHERE> eq"} introduces a
    3.21    syntactic constant which is associated with a certain term according
    3.22    to the meta-level equality @{text eq}.
     4.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Mar 30 13:40:19 2013 +0100
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Mar 30 14:57:06 2013 +0100
     4.3 @@ -781,8 +781,14 @@
     4.4        Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
     4.5  
     4.6  val _ =
     4.7 +  Outer_Syntax.improper_command @{command_spec "print_defn_rules"}
     4.8 +    "print definitional rewrite rules of context"
     4.9 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    4.10 +      Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of)));
    4.11 +
    4.12 +val _ =
    4.13    Outer_Syntax.improper_command @{command_spec "print_abbrevs"}
    4.14 -    "print constant abbreviation of context"
    4.15 +    "print constant abbreviations of context"
    4.16      (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    4.17        Toplevel.keep (Proof_Context.print_abbrevs o Toplevel.context_of)));
    4.18  
     5.1 --- a/src/Pure/Isar/local_defs.ML	Sat Mar 30 13:40:19 2013 +0100
     5.2 +++ b/src/Pure/Isar/local_defs.ML	Sat Mar 30 14:57:06 2013 +0100
     5.3 @@ -169,7 +169,7 @@
     5.4  
     5.5  (** defived definitions **)
     5.6  
     5.7 -(* transformation rules *)
     5.8 +(* transformation via rewrite rules *)
     5.9  
    5.10  structure Rules = Generic_Data
    5.11  (
    5.12 @@ -180,7 +180,7 @@
    5.13  );
    5.14  
    5.15  fun print_rules ctxt =
    5.16 -  Pretty.writeln (Pretty.big_list "definitional transformations:"
    5.17 +  Pretty.writeln (Pretty.big_list "definitional rewrite rules:"
    5.18      (map (Display.pretty_thm_item ctxt) (Rules.get (Context.Proof ctxt))));
    5.19  
    5.20  val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm);
     6.1 --- a/src/Pure/Pure.thy	Sat Mar 30 13:40:19 2013 +0100
     6.2 +++ b/src/Pure/Pure.thy	Sat Mar 30 14:57:06 2013 +0100
     6.3 @@ -75,7 +75,7 @@
     6.4    and "back" :: prf_script % "proof"
     6.5    and "Isabelle.command" :: control
     6.6    and "help" "print_commands" "print_configs"
     6.7 -    "print_context" "print_theory" "print_syntax" "print_abbrevs"
     6.8 +    "print_context" "print_theory" "print_syntax" "print_abbrevs" "print_defn_rules"
     6.9      "print_theorems" "print_locales" "print_classes" "print_locale"
    6.10      "print_interps" "print_dependencies" "print_attributes"
    6.11      "print_simpset" "print_rules" "print_trans_rules" "print_methods"