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