# HG changeset patch
# User wenzelm
# Date 1130531264 -7200
# Node ID 99d170aebb6ea3686e45eb25ca130180909a0672
# Parent  d23a846598d2653f9cfbe30f2f919a6ee81e8b01
literal facts;

diff -r d23a846598d2 -r 99d170aebb6e doc-src/IsarRef/isar-ref.tex
--- a/doc-src/IsarRef/isar-ref.tex	Fri Oct 28 22:27:41 2005 +0200
+++ b/doc-src/IsarRef/isar-ref.tex	Fri Oct 28 22:27:44 2005 +0200
@@ -44,6 +44,9 @@
 \railalias{prop}{\railqtok{prop}}
 \railalias{atom}{\railqtok{atom}}
 
+\chardef\charbackquote=`\`
+\newcommand{\backquote}{\mbox{\tt\charbackquote}}
+
 \newcommand{\drv}{\mathrel{\vdash}}
 \newcommand{\edrv}{\mathop{\drv}\nolimits}
 \newcommand{\Or}{\mathrel{\;|\;}}
diff -r d23a846598d2 -r 99d170aebb6e doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Fri Oct 28 22:27:41 2005 +0200
+++ b/doc-src/IsarRef/pure.tex	Fri Oct 28 22:27:44 2005 +0200
@@ -1026,13 +1026,14 @@
 object-logic specific tools and packages (see chapters \ref{ch:gen-tools} and
 \ref{ch:logics}).
 
-\indexisarmeth{$-$}\indexisarmeth{assumption}
+\indexisarmeth{$-$}\indexisarmeth{fact}\indexisarmeth{assumption}
 \indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{iprover}
 \indexisarattof{Pure}{intro}\indexisarattof{Pure}{elim}
 \indexisarattof{Pure}{dest}\indexisarattof{Pure}{rule}
 \indexisaratt{OF}\indexisaratt{of}\indexisaratt{where}
 \begin{matharray}{rcl}
   - & : & \isarmeth \\
+  fact & : & \isarmeth \\
   assumption & : & \isarmeth \\
   this & : & \isarmeth \\
   rule & : & \isarmeth \\
@@ -1047,6 +1048,8 @@
 \end{matharray}
 
 \begin{rail}
+  'fact' thmrefs?
+  ;
   'rule' thmrefs?
   ;
   'iprover' ('!' ?) (rulemod *)
@@ -1073,6 +1076,14 @@
   \emph{do-nothing} proof step would be ``$\PROOF{-}$'' rather than
   $\PROOFNAME$ alone.
   
+\item [$fact~\vec a$] composes any previous fact from $\vec a$ (or implicitly
+  from the current proof context) modulo matching of schematic type and term
+  variables.  The rule structure is not taken into account, i.e.\ meta-level
+  implication is considered atomic.  This is the same principle underlying
+  literal facts (cf.\ \S\ref{sec:syn-att}): ``$\HAVE{}{\phi}~\BY{fact}$'' is
+  equivalent to ``$\NOTE{}{\backquote\phi\backquote}$'' provided that $\edrv
+  \phi$ is an instance of some known $\edrv \phi$ in the proof context.
+  
 \item [$assumption$] solves some goal by a single assumption step.  All given
   facts are guaranteed to participate in the refinement; this means there may
   be only $0$ or $1$ in the first place.  Recall that $\QEDNAME$ (see
diff -r d23a846598d2 -r 99d170aebb6e doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Fri Oct 28 22:27:41 2005 +0200
+++ b/doc-src/IsarRef/syntax.tex	Fri Oct 28 22:27:44 2005 +0200
@@ -69,7 +69,8 @@
 
 \indexoutertoken{ident}\indexoutertoken{longident}\indexoutertoken{symident}
 \indexoutertoken{nat}\indexoutertoken{var}\indexoutertoken{typefree}
-\indexoutertoken{typevar}\indexoutertoken{string}\indexoutertoken{verbatim}
+\indexoutertoken{typevar}\indexoutertoken{string}\indexoutertoken{altstring}
+\indexoutertoken{verbatim}
 \begin{matharray}{rcl}
   ident & = & letter\,quasiletter^* \\
   longident & = & ident (\verb,.,ident)^+ \\
@@ -79,6 +80,7 @@
   typefree & = & \verb,',ident \\
   typevar & = & typefree ~|~ \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\
   string & = & \verb,", ~\dots~ \verb,", \\
+  altstring & = & \backquote ~\dots~ \backquote \\
   verbatim & = & \verb,{*, ~\dots~ \verb,*}, \\[1ex]
 
   letter & = & latin ~|~ \verb,\<,latin\verb,>, ~|~ \verb,\<,latin\,latin\verb,>, ~|~ greek ~|~ \\
@@ -102,10 +104,11 @@
 
 The syntax of $string$ admits any characters, including newlines; ``\verb|"|''
 (double-quote) and ``\verb|\|'' (backslash) need to be escaped by a backslash.
-The body of $verbatim$ may consist of any text not containing ``\verb|*}|'';
-this allows convenient inclusion of quotes without further escapes.  The greek
-letters do \emph{not} include \verb,\<lambda>,, which is already used
-differently in the meta-logic.
+Alternative strings according to $altstring$ are analogous, using single
+back-quotes instead.  The body of $verbatim$ may consist of any text not
+containing ``\verb|*}|''; this allows convenient inclusion of quotes without
+further escapes.  The greek letters do \emph{not} include \verb,\<lambda>,,
+which is already used differently in the meta-logic.
 
 Common mathematical symbols such as $\forall$ are represented in Isabelle as
 \verb,\<forall>,.  There are infinitely many legal symbols like this, although
@@ -338,10 +341,14 @@
 \railnonterm{thmdecl} usually refer to axioms, assumptions or results of goal
 statements, while \railnonterm{thmdef} collects lists of existing theorems.
 Existing theorems are given by \railnonterm{thmref} and \railnonterm{thmrefs},
-the former requires an actual singleton result.  An optional index selection
-specifies the individual theorems to be picked out of a given fact list.  Any
-kind of theorem specification may include lists of attributes both on the left
-and right hand sides; attributes are applied to any immediately preceding
+the former requires an actual singleton result.  There are three forms of
+theorem references: (1) named facts $a$, (2) selections from named facts $a(i,
+j - k)$, or (3) literal fact propositions using $altstring$ syntax
+$\backquote\phi\backquote$, (see also method $fact$ in
+\S\ref{sec:pure-meth-att}).
+
+Any kind of theorem specification may include lists of attributes both on the
+left and right hand sides; attributes are applied to any immediately preceding
 fact.  If names are omitted, the theorems are not stored within the theorem
 database of the theory or proof context, but any given attributes are applied
 nonetheless.
@@ -356,7 +363,7 @@
   ;
   thmdef: thmbind '='
   ;
-  thmref: nameref selection? attributes?
+  thmref: (nameref selection? | altstring) attributes?
   ;
   thmrefs: thmref +
   ;