src/Doc/IsarRef/Document_Preparation.thy
changeset 54705 0dff3326d12a
parent 54702 3daeba5130f0
child 55029 61a6bf7d4b02
     1.1 --- a/src/Doc/IsarRef/Document_Preparation.thy	Mon Dec 09 12:27:18 2013 +0100
     1.2 +++ b/src/Doc/IsarRef/Document_Preparation.thy	Mon Dec 09 20:16:12 2013 +0100
     1.3 @@ -177,6 +177,7 @@
     1.4        @@{antiquotation ML_type} options @{syntax name} |
     1.5        @@{antiquotation ML_struct} options @{syntax name} |
     1.6        @@{antiquotation \"file\"} options @{syntax name} |
     1.7 +      @@{antiquotation file_unchecked} options @{syntax name} |
     1.8        @@{antiquotation url} options @{syntax name}
     1.9      ;
    1.10      options: '[' (option * ',') ']'
    1.11 @@ -269,6 +270,10 @@
    1.12    \item @{text "@{file path}"} checks that @{text "path"} refers to a
    1.13    file (or directory) and prints it verbatim.
    1.14  
    1.15 +  \item @{text "@{file_unchecked path}"} is like @{text "@{file
    1.16 +  path}"}, but does not check the existence of the @{text "path"}
    1.17 +  within the file-system.
    1.18 +
    1.19    \item @{text "@{url name}"} produces markup for the given URL, which
    1.20    results in an active hyperlink within the text.
    1.21