presentation tuned decompose-isar
authorMathias Lehnfeld <e0726734@student.tuwien.ac.at>
Sun, 29 May 2011 12:53:49 +0200
branchdecompose-isar
changeset 420326e3504221cac
parent 42031 95abe93a41d2
child 42033 9e055a200e03
presentation tuned
doc-src/isac/mlehnfeld/presentation.tex
test/Tools/isac/ADDTESTS/All_Ctxt.thy
     1.1 --- a/doc-src/isac/mlehnfeld/presentation.tex	Sat May 28 21:41:12 2011 +0200
     1.2 +++ b/doc-src/isac/mlehnfeld/presentation.tex	Sun May 29 12:53:49 2011 +0200
     1.3 @@ -232,8 +232,8 @@
     1.4        src/Pure/ & 70 k \\
     1.5        src/Provers/ & 8 k \\
     1.6        src/Tools/ & 800 k \\
     1.7 -      src/isac/ & 37 k \\
     1.8 -      src/isac/Knowledge & 16 k \\
     1.9 +      src/Tools/isac/ & 37 k \\
    1.10 +      src/Tools/isac/Knowledge & 16 k \\
    1.11      \end{tabular}
    1.12  \end{frame}
    1.13  
    1.14 @@ -302,7 +302,7 @@
    1.15    \frametitle{Preparation of Future Development}
    1.16      \begin{itemize}
    1.17      \item logical data for Isabelle provers in contexts
    1.18 -    \item \isac programming language more compact\\
    1.19 +    \item \isac{} programming language more compact\\
    1.20        $\rightarrow$ context built automatically
    1.21      \end{itemize}
    1.22  \end{frame}
     2.1 --- a/test/Tools/isac/ADDTESTS/All_Ctxt.thy	Sat May 28 21:41:12 2011 +0200
     2.2 +++ b/test/Tools/isac/ADDTESTS/All_Ctxt.thy	Sun May 29 12:53:49 2011 +0200
     2.3 @@ -12,7 +12,6 @@
     2.4      ("Test", ["sqroot-test","univariate","equation","test"],
     2.5       ["Test","squ-equ-test-subpbl1"]);
     2.6    val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
     2.7 -  show_pt pt;
     2.8  *}
     2.9  
    2.10  section {* start of specify phase *}
    2.11 @@ -120,4 +119,8 @@
    2.12    terms2strs (get_assumptions_ pt p);
    2.13  *}
    2.14  
    2.15 +ML {*
    2.16 +  show_pt pt;
    2.17 +*}
    2.18 +
    2.19  end
    2.20 \ No newline at end of file