1.1 --- a/ROOT	Sun Jul 13 08:17:09 2014 +0200
     1.2 +++ b/ROOT	Wed Jan 08 11:20:20 2020 +0100
     1.3 @@ -1,14 +1,15 @@
     1.4  session "Risc_Workshop_Paper" = "HOL" +
     1.5    options [document = pdf, document_output = "output"]
     1.6    theories [document = false]
     1.7 -    "~~/src/HOL/Library/Polynomial"
     1.8 -    "~~/src/HOL/Algebra/UnivPoly"
     1.9 -    "~~/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff"
    1.10 -    "~~/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial"
    1.11 -    "~~/src/HOL/Decision_Procs/Commutative_Ring"
    1.12 +    "/usr/local/isabisac14/src/HOL/Library/Polynomial"
    1.13 +    "/usr/local/isabisac14/src/HOL/Algebra/UnivPoly"
    1.14 +    "/usr/local/isabisac14/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff"
    1.15 +    "/usr/local/isabisac14/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial"
    1.16 +    "/usr/local/isabisac14/src/HOL/Decision_Procs/Commutative_Ring"
    1.17    theories [quick_and_dirty, document = false]
    1.18 -    "../risc-poly/MPoly"
    1.19 +    "../poly/MPoly"
    1.20    theories
    1.21      "Motivation"
    1.22      "MPoly_Bootstrap"
    1.23 -  files "document/root.tex"
    1.24 +  document_files
    1.25 +    "root.tex"

     2.1 --- a/build	Sun Jul 13 08:17:09 2014 +0200
     2.2 +++ b/build	Wed Jan 08 11:20:20 2020 +0100
     2.3 @@ -1,5 +1,11 @@
     2.4  #!/bin/bash
     2.5  
     2.6 +###WN: raises
     2.7 +###WN: ! LaTeX Error: File `output/document/Motivation.tex' not found.
     2.8 +###WN: 
     2.9 +###WN: ? how is `output/document/Motivation.tex' generated 
    2.10 +###WN: ? from   `Motivation.thy' ???
    2.11 +
    2.12  ## note: check with bash -n
    2.13  
    2.14  ## prelude

     3.1 --- a/build_thy	Sun Jul 13 08:17:09 2014 +0200
     3.2 +++ b/build_thy	Wed Jan 08 11:20:20 2020 +0100
     3.3 @@ -1,3 +1,22 @@
     3.4  #!/bin/bash
     3.5  
     3.6 -exec "$(dirname "$0")"/isabelle build -D .
     3.7 +#exec "$(dirname "$0")"/isabelle build -D .
     3.8 +
     3.9 +#WN...
    3.10 +exec /usr/local/isabisac14/bin/isabelle build -D .
    3.11 +#WN still with errors:
    3.12 +# wneuper@wneuper-w541:~/repos/polypaper$ ./build_thy 
    3.13 +# ### Missing Isabelle component: "/home/wneuper/.isabelle/contrib/cvc3-2.4.1"
    3.14 +# ### Missing Isabelle component: "/home/wneuper/.isabelle/contrib/Haskabelle-2014"
    3.15 +# ### Missing Isabelle component: "/home/wneuper/.isabelle/contrib/polyml-5.5.2-1"
    3.16 +# ### Missing Isabelle component: "/home/wneuper/.isabelle/contrib/scala-2.11.2"
    3.17 +# ### Missing Isabelle component: "/home/wneuper/.isabelle/contrib/z3-3.2-1"
    3.18 +# ### Missing Isabelle component: "/home/wneuper/.isabelle/contrib/z3-4.3.2pre-1"
    3.19 +# *** Incoherent imports for theory "MPoly":
    3.20 +# ***   "../risc-poly/MPoly.thy" (file "MPoly_Bootstrap.thy")
    3.21 +# ***   "../risc-poly/MPoly.thy" (line 1 of "ROOT")
    3.22 +# ***   "../poly/MPoly.thy" (file "MPoly_Bootstrap.thy")
    3.23 +# ***   "../poly/MPoly.thy" (line 1 of "ROOT")
    3.24 +# *** The error(s) above occurred in session "Risc_Workshop_Paper" (line 1 of "ROOT")
    3.25 +# 0:00:03 elapsed time, 0:00:06 cpu time
    3.26 +# wneuper@wneuper-w541:~/repos/polypaper$ 

     4.1 --- a/dict/.aspell.en.pws	Sun Jul 13 08:17:09 2014 +0200
     4.2 +++ b/dict/.aspell.en.pws	Wed Jan 08 11:20:20 2020 +0100
     4.3 @@ -1,4 +1,4 @@
     4.4 -personal_ws-1.1 en 88 
     4.5 +personal_ws-1.1 en 94 
     4.6  sep
     4.7  sym
     4.8  reifying
     4.9 @@ -30,12 +30,15 @@
    4.10  coeff
    4.11  lex
    4.12  recurse
    4.13 +provers
    4.14  impl
    4.15  algebraists
    4.16  Modellierung
    4.17 +parametrised
    4.18  Typeclass
    4.19  keine
    4.20  eq
    4.21 +isomorphism
    4.22  TODO
    4.23  automatische
    4.24  lookup
    4.25 @@ -64,11 +67,14 @@
    4.26  implT
    4.27  CTP
    4.28  ueber
    4.29 +invariants
    4.30  ungeeignet
    4.31  yshift
    4.32  logisch
    4.33  Repraesentationen
    4.34 +subtype
    4.35  Gleichung
    4.36 +monomial
    4.37  xpl
    4.38  Kombination
    4.39  datatype