Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
isa-afp
afp-2020
Commits
9ab9ebc9de46
Commit
c562c3e3
authored
Dec 09, 2013
by
wenzelm
Browse files
more antiquotations;
parent
d41788337158
Changes
9
Hide whitespace changes
Inline
Side-by-side
thys/Circus/Refinement.thy
View file @
9ab9ebc9
...
...
@@ -26,7 +26,7 @@ test-cases, which we adress in the future).
In order to enter Isabelle/\Circus specifications, an own parser has
been developed (the the interested reader is referred to:
\
url
{
http://www.lri.fr/~feliachi/IsabelleCircus/}). In the
@{
url
"
http://www.lri.fr/~feliachi/IsabelleCircus/
"
}). In the
following, we will present our example both in high-level syntax
implementing common textbook notation on \Circus\ as well as the
semantic code resulting from these expressions in the context of
...
...
thys/Collections/Examples/Refine_Monadic/Bfs_Impl.thy
View file @
9ab9ebc9
...
...
@@ -21,7 +21,7 @@ begin
Isabelle/HOLs code generator to generate ML-code.
The implementation uses the Isabelle Collection Framework (ICF)
(Available at
\
url
{
http://afp.sourceforge.net/entries/Collections.shtml}),
(Available at
@{
url
"
http://afp.sourceforge.net/entries/Collections.shtml
"
}),
to provide efficient set implementations. We choose a hashset
(backed by a Red Black Tree) for the visited set, and lists for
all other sets. Moreover, we fix the node type to natural numbers.
...
...
thys/Collections/Userguides/ICF_Userguide.thy
View file @
9ab9ebc9
...
...
@@ -404,7 +404,7 @@ text_raw {*\label{sec:userguide.design}*}
For a more detailed discussion of the data refinement issue, we refer to
the monadic refinement framework, that is available in the AFP
(
\
url
{
http://afp.sourceforge.net/entries/Refine_Monadic.shtml})
(
@{
url
"
http://afp.sourceforge.net/entries/Refine_Monadic.shtml
"
})
*}
subsection {* Operation Records *}
...
...
thys/Efficient-Mergesort/Efficient_Sort.thy
View file @
9ab9ebc9
...
...
@@ -144,7 +144,7 @@ section {* GHC Version of Mergesort *}
text {*
In the following we show that the mergesort implementation
used in GHC (see
\
url
{
http://haskell.org/ghc/docs/7.0-latest/html/libraries/base-4.3.1.0/src/Data-List.html#sort})
used in GHC (see
@{
url
"
http://haskell.org/ghc/docs/7.0-latest/html/libraries/base-4.3.1.0/src/Data-List.html#sort
"
})
is a correct and stable sorting algorithm. Furthermore, experimental
data suggests that generated code for this implementation is much more
efficient than for the implementation provided by @{theory Multiset}.
...
...
thys/Example-Submission/Submission.thy
View file @
9ab9ebc9
...
...
@@ -36,7 +36,7 @@ text {*
\end{itemize}
The submission of the example you are reading is at
\
url
{
http://afp.sf.net/release/afp-Example-Submission-current.tar.gz}.
@{
url
"
http://afp.sf.net/release/afp-Example-Submission-current.tar.gz
"
}.
*}
section "Proof styles"
...
...
thys/GoedelGod/GoedelGod.thy
View file @
9ab9ebc9
...
...
@@ -27,13 +27,13 @@ section {* Introduction *}
Isabelle is described in the textbook by Nipkow,
Paulson, and Wenzel \cite{Isabelle} and in tutorials available
at:
\
url
{
http://isabelle.in.tum.de}.
at:
@{
url
"
http://isabelle.in.tum.de
"
}.
\subsection{Related Work}
The formalization presented here is related to the THF \cite{J22} and
Coq \cite{Coq} formalizations at
\
url
{
https://github.com/FormalTheology/GoedelGod/tree/master/Formalizations/}.
@{
url
"
https://github.com/FormalTheology/GoedelGod/tree/master/Formalizations/
"
}.
An older ontological argument by Anselm was formalized in PVS by John Rushby \cite{rushby}.
*}
...
...
thys/HereditarilyFinite/OrdArith.thy
View file @
9ab9ebc9
...
...
@@ -6,7 +6,7 @@ begin
section {*Generalised Addition --- Also for Ordinals *}
text{*Source: Laurence Kirby, Addition and multiplication of sets
Math. Log. Quart. 53, No. 1, 52 – 65 (2007) / DOI 10.1002/malq.200610026
http://faculty.baruch.cuny.edu/lkirby/mlqarticlejan2007.pdf*}
@{url "
http://faculty.baruch.cuny.edu/lkirby/mlqarticlejan2007.pdf
"}
*}
definition
hadd :: "hf \<Rightarrow> hf \<Rightarrow> hf" (infixl "@+" 65) where
...
...
thys/JinjaThreads/Common/ExternalCall.thy
View file @
9ab9ebc9
...
...
@@ -131,9 +131,9 @@ text {*
because the interrupt flag is not stored inside the thread object.
Starting a clone of a started thread with Sun JVM 1.6.0\_07 raises an illegal thread state exception,
we just start another thread.
The thread at
\texttt{
http://mail.openjdk.java.net/pipermail/core-libs-dev/2010-August/004715.html} discusses
The thread at
@{url "
http://mail.openjdk.java.net/pipermail/core-libs-dev/2010-August/004715.html
"
} discusses
the general problem of thread cloning and argues against that.
The bug report
\texttt{
http://bugs.sun.com/bugdatabase/view
\
_bug.do?bug
\
_id=6968584}
The bug report
@{url "
http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=6968584
"
}
changes the Thread class implementation
such that \texttt{Object.clone()} can no longer be accessed for Thread and subclasses in Java 7.
...
...
thys/Refine_Monadic/examples/Breadth_First_Search.thy
View file @
9ab9ebc9
...
...
@@ -6,7 +6,7 @@ begin
text {*
This is a slightly modified version of Task~5 of our submission to
the VSTTE 2011 verification competition
(
\
url
{
https://sites.google.com/site/vstte2012/compet}). The task was to
(
@{
url
"
https://sites.google.com/site/vstte2012/compet
"
}). The task was to
formalize a breadth-first-search algorithm.
*}
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment