--- a/doc-src/IsarRef/Thy/Generic.thy Wed May 14 20:30:53 2008 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy Wed May 14 20:31:17 2008 +0200
@@ -1,7 +1,7 @@
(* $Id$ *)
theory Generic
-imports CPure
+imports Main
begin
chapter {* Generic tools and packages \label{ch:gen-tools} *}
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed May 14 20:30:53 2008 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed May 14 20:31:17 2008 +0200
@@ -53,10 +53,10 @@
corresponding injection/surjection pair (in both directions). Rules
@{text Rep_t_inject} and @{text Abs_t_inject} provide a slightly
more convenient view on the injectivity part, suitable for automated
- proof tools (e.g.\ in @{method simp} or @{method iff} declarations).
- Rules @{text Rep_t_cases}/@{text Rep_t_induct}, and @{text
- Abs_t_cases}/@{text Abs_t_induct} provide alternative views on
- surjectivity; these are already declared as set or type rules for
+ proof tools (e.g.\ in @{attribute simp} or @{attribute iff}
+ declarations). Rules @{text Rep_t_cases}/@{text Rep_t_induct}, and
+ @{text Abs_t_cases}/@{text Abs_t_induct} provide alternative views
+ on surjectivity; these are already declared as set or type rules for
the generic @{method cases} and @{method induct} methods.
An alternative name may be specified in parentheses; the default is
@@ -89,7 +89,7 @@
\begin{descr}
- \item [@{method (HOL) split_format}~@{text "p\<^sub>1 \<dots> p\<^sub>m
+ \item [@{attribute (HOL) split_format}~@{text "p\<^sub>1 \<dots> p\<^sub>m
\<AND> \<dots> \<AND> q\<^sub>1 \<dots> q\<^sub>n"}] puts expressions of
low-level tuple types into canonical form as specified by the
arguments given; the @{text i}-th collection of arguments refers to
@@ -813,15 +813,15 @@
text {*
\begin{matharray}{rcl}
@{method_def (HOL) arith} & : & \isarmeth \\
- @{method_def (HOL) arith_split} & : & \isaratt \\
+ @{attribute_def (HOL) arith_split} & : & \isaratt \\
\end{matharray}
The @{method (HOL) arith} method decides linear arithmetic problems
(on types @{text nat}, @{text int}, @{text real}). Any current
facts are inserted into the goal before running the procedure.
- The @{method (HOL) arith_split} attribute declares case split rules
- to be expanded before the arithmetic procedure is invoked.
+ The @{attribute (HOL) arith_split} attribute declares case split
+ rules to be expanded before the arithmetic procedure is invoked.
Note that a simpler (but faster) version of arithmetic reasoning is
already performed by the Simplifier.
--- a/doc-src/IsarRef/Thy/Proof.thy Wed May 14 20:30:53 2008 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy Wed May 14 20:31:17 2008 +0200
@@ -784,7 +784,7 @@
multi-step tactic script for @{command "qed"}, but may be given
anywhere within the proof body.
- No facts are passed to @{method m} here. Furthermore, the static
+ No facts are passed to @{text m} here. Furthermore, the static
context is that of the enclosing goal (as for actual @{command
"qed"}). Thus the proof method may not refer to any assumptions
introduced in the current body, for example.
@@ -1020,7 +1020,7 @@
\item [@{attribute trans}] declares theorems as transitivity rules.
\item [@{attribute sym}] declares symmetry rules, as well as
- @{attribute "Pure.elim?"} rules.
+ @{attribute "Pure.elim"}@{text "?"} rules.
\item [@{attribute symmetric}] resolves a theorem with some rule
declared as @{attribute sym} in the current context. For example,
--- a/doc-src/IsarRef/Thy/ZF_Specific.thy Wed May 14 20:30:53 2008 +0200
+++ b/doc-src/IsarRef/Thy/ZF_Specific.thy Wed May 14 20:31:17 2008 +0200
@@ -1,7 +1,7 @@
(* $Id$ *)
theory ZF_Specific
-imports ZF
+imports Main
begin
chapter {* Isabelle/ZF \label{ch:zf} *}
--- a/doc-src/IsarRef/Thy/pure.thy Wed May 14 20:30:53 2008 +0200
+++ b/doc-src/IsarRef/Thy/pure.thy Wed May 14 20:31:17 2008 +0200
@@ -731,7 +731,7 @@
@{command_def "print_attributes"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
@{command_def "print_theorems"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
@{command_def "find_theorems"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
- @{command_def "thms_deps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+ @{command_def "thm_deps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
@{command_def "print_facts"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\
@{command_def "print_binds"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\
\end{matharray}
@@ -795,7 +795,7 @@
yields \emph{all} currently known facts. An optional limit for the
number of printed facts may be given; the default is 40. By
default, duplicates are removed from the search result. Use
- @{keyword "with_dups"} to display duplicates.
+ @{text with_dups} to display duplicates.
\item [@{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}]
visualizes dependencies of facts, using Isabelle's graph browser
--- a/doc-src/antiquote_setup.ML Wed May 14 20:30:53 2008 +0200
+++ b/doc-src/antiquote_setup.ML Wed May 14 20:31:17 2008 +0200
@@ -138,42 +138,50 @@
local
+fun no_check _ _ = true;
+
+fun thy_check intern defined ctxt =
+ let val thy = ProofContext.theory_of ctxt
+ in defined thy o intern thy end;
+
val arg = enclose "{" "}" o clean_string;
-fun output_entity markup index kind ctxt (logic, name) =
- (case index of
- NONE => ""
- | SOME is_def =>
- "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name)
- ^
- (Output.output name
- |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
- |> (if ! O.quotes then quote else I)
- |> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
- else enclose "\\mbox{\\isa{" "}}"));
+fun output_entity check markup index kind ctxt (logic, name) =
+ if check ctxt name then
+ (case index of
+ NONE => ""
+ | SOME is_def =>
+ "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name)
+ ^
+ (Output.output name
+ |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
+ |> (if ! O.quotes then quote else I)
+ |> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
+ else enclose "\\mbox{\\isa{" "}}"))
+ else error ("Undefined " ^ kind ^ " " ^ quote name);
-fun entity markup index kind =
+fun entity check markup index kind =
O.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
- (K (output_entity markup index kind));
+ (K (output_entity check markup index kind));
-fun entity_antiqs markup kind =
- [(kind, entity markup NONE kind),
- (kind ^ "_def", entity markup (SOME true) kind),
- (kind ^ "_ref", entity markup (SOME false) kind)];
+fun entity_antiqs check markup kind =
+ [(kind, entity check markup NONE kind),
+ (kind ^ "_def", entity check markup (SOME true) kind),
+ (kind ^ "_ref", entity check markup (SOME false) kind)];
in
val _ = O.add_commands
- (entity_antiqs "" "syntax" @
- entity_antiqs "isacommand" "command" @
- entity_antiqs "isakeyword" "keyword" @
- entity_antiqs "isakeyword" "element" @
- entity_antiqs "" "method" @
- entity_antiqs "" "attribute" @
- entity_antiqs "" "fact" @
- entity_antiqs "" "variable" @
- entity_antiqs "" "case" @
- entity_antiqs "" "antiquotation");
+ (entity_antiqs no_check "" "syntax" @
+ entity_antiqs (K (is_some o OuterSyntax.command_keyword)) "isacommand" "command" @
+ entity_antiqs (K OuterSyntax.is_keyword) "isakeyword" "keyword" @
+ entity_antiqs (K OuterSyntax.is_keyword) "isakeyword" "element" @
+ entity_antiqs (thy_check Method.intern Method.defined) "" "method" @
+ entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute" @
+ entity_antiqs no_check "" "fact" @
+ entity_antiqs no_check "" "variable" @
+ entity_antiqs no_check "" "case" @
+ entity_antiqs (K ThyOutput.defined_command) "" "antiquotation");
end;