1.1 --- a/doc-src/IsarRef/Thy/Generic.thy	Wed May 14 20:30:53 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Generic.thy	Wed May 14 20:31:17 2008 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  (* $Id$ *)
     1.5  
     1.6  theory Generic
     1.7 -imports CPure
     1.8 +imports Main
     1.9  begin
    1.10  
    1.11  chapter {* Generic tools and packages \label{ch:gen-tools} *}

     2.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed May 14 20:30:53 2008 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed May 14 20:31:17 2008 +0200
     2.3 @@ -53,10 +53,10 @@
     2.4    corresponding injection/surjection pair (in both directions).  Rules
     2.5    @{text Rep_t_inject} and @{text Abs_t_inject} provide a slightly
     2.6    more convenient view on the injectivity part, suitable for automated
     2.7 -  proof tools (e.g.\ in @{method simp} or @{method iff} declarations).
     2.8 -  Rules @{text Rep_t_cases}/@{text Rep_t_induct}, and @{text
     2.9 -  Abs_t_cases}/@{text Abs_t_induct} provide alternative views on
    2.10 -  surjectivity; these are already declared as set or type rules for
    2.11 +  proof tools (e.g.\ in @{attribute simp} or @{attribute iff}
    2.12 +  declarations).  Rules @{text Rep_t_cases}/@{text Rep_t_induct}, and
    2.13 +  @{text Abs_t_cases}/@{text Abs_t_induct} provide alternative views
    2.14 +  on surjectivity; these are already declared as set or type rules for
    2.15    the generic @{method cases} and @{method induct} methods.
    2.16    
    2.17    An alternative name may be specified in parentheses; the default is
    2.18 @@ -89,7 +89,7 @@
    2.19  
    2.20    \begin{descr}
    2.21    
    2.22 -  \item [@{method (HOL) split_format}~@{text "p\<^sub>1 \<dots> p\<^sub>m
    2.23 +  \item [@{attribute (HOL) split_format}~@{text "p\<^sub>1 \<dots> p\<^sub>m
    2.24    \<AND> \<dots> \<AND> q\<^sub>1 \<dots> q\<^sub>n"}] puts expressions of
    2.25    low-level tuple types into canonical form as specified by the
    2.26    arguments given; the @{text i}-th collection of arguments refers to
    2.27 @@ -813,15 +813,15 @@
    2.28  text {*
    2.29    \begin{matharray}{rcl}
    2.30      @{method_def (HOL) arith} & : & \isarmeth \\
    2.31 -    @{method_def (HOL) arith_split} & : & \isaratt \\
    2.32 +    @{attribute_def (HOL) arith_split} & : & \isaratt \\
    2.33    \end{matharray}
    2.34  
    2.35    The @{method (HOL) arith} method decides linear arithmetic problems
    2.36    (on types @{text nat}, @{text int}, @{text real}).  Any current
    2.37    facts are inserted into the goal before running the procedure.
    2.38  
    2.39 -  The @{method (HOL) arith_split} attribute declares case split rules
    2.40 -  to be expanded before the arithmetic procedure is invoked.
    2.41 +  The @{attribute (HOL) arith_split} attribute declares case split
    2.42 +  rules to be expanded before the arithmetic procedure is invoked.
    2.43  
    2.44    Note that a simpler (but faster) version of arithmetic reasoning is
    2.45    already performed by the Simplifier.

     3.1 --- a/doc-src/IsarRef/Thy/Proof.thy	Wed May 14 20:30:53 2008 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/Proof.thy	Wed May 14 20:31:17 2008 +0200
     3.3 @@ -784,7 +784,7 @@
     3.4    multi-step tactic script for @{command "qed"}, but may be given
     3.5    anywhere within the proof body.
     3.6    
     3.7 -  No facts are passed to @{method m} here.  Furthermore, the static
     3.8 +  No facts are passed to @{text m} here.  Furthermore, the static
     3.9    context is that of the enclosing goal (as for actual @{command
    3.10    "qed"}).  Thus the proof method may not refer to any assumptions
    3.11    introduced in the current body, for example.
    3.12 @@ -1020,7 +1020,7 @@
    3.13    \item [@{attribute trans}] declares theorems as transitivity rules.
    3.14  
    3.15    \item [@{attribute sym}] declares symmetry rules, as well as
    3.16 -  @{attribute "Pure.elim?"} rules.
    3.17 +  @{attribute "Pure.elim"}@{text "?"} rules.
    3.18  
    3.19    \item [@{attribute symmetric}] resolves a theorem with some rule
    3.20    declared as @{attribute sym} in the current context.  For example,

     4.1 --- a/doc-src/IsarRef/Thy/ZF_Specific.thy	Wed May 14 20:30:53 2008 +0200
     4.2 +++ b/doc-src/IsarRef/Thy/ZF_Specific.thy	Wed May 14 20:31:17 2008 +0200
     4.3 @@ -1,7 +1,7 @@
     4.4  (* $Id$ *)
     4.5  
     4.6  theory ZF_Specific
     4.7 -imports ZF
     4.8 +imports Main
     4.9  begin
    4.10  
    4.11  chapter {* Isabelle/ZF \label{ch:zf} *}

     5.1 --- a/doc-src/IsarRef/Thy/pure.thy	Wed May 14 20:30:53 2008 +0200
     5.2 +++ b/doc-src/IsarRef/Thy/pure.thy	Wed May 14 20:31:17 2008 +0200
     5.3 @@ -731,7 +731,7 @@
     5.4      @{command_def "print_attributes"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
     5.5      @{command_def "print_theorems"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
     5.6      @{command_def "find_theorems"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
     5.7 -    @{command_def "thms_deps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
     5.8 +    @{command_def "thm_deps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
     5.9      @{command_def "print_facts"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\
    5.10      @{command_def "print_binds"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\
    5.11    \end{matharray}
    5.12 @@ -795,7 +795,7 @@
    5.13    yields \emph{all} currently known facts.  An optional limit for the
    5.14    number of printed facts may be given; the default is 40.  By
    5.15    default, duplicates are removed from the search result. Use
    5.16 -  @{keyword "with_dups"} to display duplicates.
    5.17 +  @{text with_dups} to display duplicates.
    5.18    
    5.19    \item [@{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}]
    5.20    visualizes dependencies of facts, using Isabelle's graph browser

     6.1 --- a/doc-src/antiquote_setup.ML	Wed May 14 20:30:53 2008 +0200
     6.2 +++ b/doc-src/antiquote_setup.ML	Wed May 14 20:31:17 2008 +0200
     6.3 @@ -138,42 +138,50 @@
     6.4  
     6.5  local
     6.6  
     6.7 +fun no_check _ _ = true;
     6.8 +
     6.9 +fun thy_check intern defined ctxt =
    6.10 +  let val thy = ProofContext.theory_of ctxt
    6.11 +  in defined thy o intern thy end;
    6.12 +
    6.13  val arg = enclose "{" "}" o clean_string;
    6.14  
    6.15 -fun output_entity markup index kind ctxt (logic, name) =
    6.16 -  (case index of
    6.17 -    NONE => ""
    6.18 -  | SOME is_def =>
    6.19 -      "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name)
    6.20 -  ^
    6.21 -  (Output.output name
    6.22 -    |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
    6.23 -    |> (if ! O.quotes then quote else I)
    6.24 -    |> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    6.25 -        else enclose "\\mbox{\\isa{" "}}"));
    6.26 +fun output_entity check markup index kind ctxt (logic, name) =
    6.27 +  if check ctxt name then
    6.28 +    (case index of
    6.29 +      NONE => ""
    6.30 +    | SOME is_def =>
    6.31 +        "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name)
    6.32 +    ^
    6.33 +    (Output.output name
    6.34 +      |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")                                    
    6.35 +      |> (if ! O.quotes then quote else I)
    6.36 +      |> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    6.37 +          else enclose "\\mbox{\\isa{" "}}"))
    6.38 +  else error ("Undefined " ^ kind ^ " " ^ quote name);
    6.39  
    6.40 -fun entity markup index kind =
    6.41 +fun entity check markup index kind =
    6.42    O.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
    6.43 -    (K (output_entity markup index kind));
    6.44 +    (K (output_entity check markup index kind));
    6.45      
    6.46 -fun entity_antiqs markup kind =
    6.47 - [(kind, entity markup NONE kind),
    6.48 -  (kind ^ "_def", entity markup (SOME true) kind), 
    6.49 -  (kind ^ "_ref", entity markup (SOME false) kind)];
    6.50 +fun entity_antiqs check markup kind =
    6.51 + [(kind, entity check markup NONE kind),
    6.52 +  (kind ^ "_def", entity check markup (SOME true) kind), 
    6.53 +  (kind ^ "_ref", entity check markup (SOME false) kind)];
    6.54  
    6.55  in
    6.56  
    6.57  val _ = O.add_commands
    6.58 - (entity_antiqs "" "syntax" @
    6.59 -  entity_antiqs "isacommand" "command" @
    6.60 -  entity_antiqs "isakeyword" "keyword" @
    6.61 -  entity_antiqs "isakeyword" "element" @
    6.62 -  entity_antiqs "" "method" @
    6.63 -  entity_antiqs "" "attribute" @
    6.64 -  entity_antiqs "" "fact" @
    6.65 -  entity_antiqs "" "variable" @
    6.66 -  entity_antiqs "" "case" @
    6.67 -  entity_antiqs "" "antiquotation");
    6.68 + (entity_antiqs no_check "" "syntax" @
    6.69 +  entity_antiqs (K (is_some o OuterSyntax.command_keyword)) "isacommand" "command" @
    6.70 +  entity_antiqs (K OuterSyntax.is_keyword) "isakeyword" "keyword" @
    6.71 +  entity_antiqs (K OuterSyntax.is_keyword) "isakeyword" "element" @
    6.72 +  entity_antiqs (thy_check Method.intern Method.defined) "" "method" @
    6.73 +  entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute" @
    6.74 +  entity_antiqs no_check "" "fact" @
    6.75 +  entity_antiqs no_check "" "variable" @
    6.76 +  entity_antiqs no_check "" "case" @
    6.77 +  entity_antiqs (K ThyOutput.defined_command) "" "antiquotation");
    6.78  
    6.79  end;
    6.80