# HG changeset patch
# User Walther Neuper <walther.neuper@jku.at>
# Date 1617535864 -7200
# Node ID 0959e61a3f3f1c6ad49f4346391268e724390cc6
# Parent  9f927860d9073d388a55c547719cfc6f1cf813b5
new session for Doc/Specify_Phase, incomplete

diff -r 9f927860d907 -r 0959e61a3f3f src/Tools/isac/Doc/Lucas_Interpreter/document/root.tex
--- a/src/Tools/isac/Doc/Lucas_Interpreter/document/root.tex	Sun Apr 04 12:29:42 2021 +0200
+++ b/src/Tools/isac/Doc/Lucas_Interpreter/document/root.tex	Sun Apr 04 13:31:04 2021 +0200
@@ -1,5 +1,5 @@
 % into "root.tex" as created by "isabelle mkdir"
-%  code from "llncs/samplepaper.tex" is inserted
+%  code from "llncs/samplepaper.tex" is inserted -- llncs NOT COMPATIBLE WITH package isabelle
 
 \documentclass{article}
 \usepackage{isabelle,isabellesym}
diff -r 9f927860d907 -r 0959e61a3f3f src/Tools/isac/Doc/README
--- a/src/Tools/isac/Doc/README	Sun Apr 04 12:29:42 2021 +0200
+++ b/src/Tools/isac/Doc/README	Sun Apr 04 13:31:04 2021 +0200
@@ -4,4 +4,4 @@
 /usr/local/isabisac/bin/isabelle build -D .
  
 In case nothing happens with the above command, go
-~/.isabelle/isabisac/heaps/polyml-5.8_x86_64_32-linux/log$ rm Lucas_Interpreter*
+~/.isabelle/isabisac/heaps/polyml-5.8_x86_64_32-linux/log$ rm Interpret*
diff -r 9f927860d907 -r 0959e61a3f3f src/Tools/isac/Doc/ROOT
--- a/src/Tools/isac/Doc/ROOT	Sun Apr 04 12:29:42 2021 +0200
+++ b/src/Tools/isac/Doc/ROOT	Sun Apr 04 13:31:04 2021 +0200
@@ -14,3 +14,17 @@
     "fun-pack-simplify.png"
     "root.bib"
     "root.tex"
+
+session "Specify_Phase" in "Specify_Phase" = HOL +
+  options [document = pdf, document_output = "output"]
+  sessions
+    "Specify"
+  theories
+    "Specify_Phase"
+  document_files (in "../")
+    "isabelle.sty"
+    "isabellesym.sty"
+    "pdfsetup.sty"
+  document_files
+    "root.bib"
+    "root.tex"
diff -r 9f927860d907 -r 0959e61a3f3f src/Tools/isac/Doc/Specify_Phase/Specify_Phase.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/isac/Doc/Specify_Phase/Specify_Phase.thy	Sun Apr 04 13:31:04 2021 +0200
@@ -0,0 +1,11 @@
+(*<*)
+(*%:wrap=soft:maxLineLen=78:*)
+theory Specify_Phase
+  imports "Specify.Specify"
+begin
+(*>*)
+
+
+(*<*)
+end
+(*>*)
\ No newline at end of file
diff -r 9f927860d907 -r 0959e61a3f3f src/Tools/isac/Doc/Specify_Phase/document/root.bib
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/isac/Doc/Specify_Phase/document/root.bib	Sun Apr 04 13:31:04 2021 +0200
@@ -0,0 +1,8 @@
+@TechReport{isac:all,
+  author = 	 {\isac{}- Team},
+  title = 	 {\isac{} -- User Requirements Document},
+  institution =  {Institute for Softwaretechnology, 
+                  University of Technology},
+  year = 	 {2002},
+  note = 	 {\url{https://static.miraheze.org/isacwiki/TODO/URD.pdf}}
+}
diff -r 9f927860d907 -r 0959e61a3f3f src/Tools/isac/Doc/Specify_Phase/document/root.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/isac/Doc/Specify_Phase/document/root.tex	Sun Apr 04 13:31:04 2021 +0200
@@ -0,0 +1,45 @@
+\documentclass{article}
+\usepackage{isabelle,isabellesym}
+\usepackage{graphicx}
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{tt}  %better readable than {it}
+
+% for uniform font size
+%\renewcommand{\isastyle}{\isastyleminor}
+
+\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
+\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
+
+\begin{document}
+
+\title{The Specify Phase in \isac's Calculations}
+\author{Walther Neuper}
+%\institute{Johannes Kepler University, Linz, Austria}
+\maketitle
+\vspace{2cm}
+\tableofcontents
+\newpage
+
+% sane default for proof documents
+\parindent 0pt\parskip 0.5ex
+
+% generated text of all theories
+\input{Specify_Phase.tex}  %*.tex created by isabelle build
+
+% optional bibliography
+\bibliographystyle{plain}
+% \bibliographystyle{splncs04}
+% splncs04 CAUSES ERROR
+% SEE ~/material/templates/llncs/README
+\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End: