update protocol decompose-isar
authorAlexander Kargl <akargl@brgkepler.net>
Thu, 14 Jul 2011 10:01:33 +0200
branchdecompose-isar
changeset 4208451d39b0eb23d
parent 42081 b5a91fb4330c
child 42085 e4411330f232
update protocol
doc-src/isac/akargl/ferialprakt.tex
test/Tools/isac/ADDTESTS/course/ml_quickstart/ML1_Basics.thy
     1.1 --- a/doc-src/isac/akargl/ferialprakt.tex	Wed Jul 13 10:41:17 2011 +0200
     1.2 +++ b/doc-src/isac/akargl/ferialprakt.tex	Thu Jul 14 10:01:33 2011 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  \title{Ferialpraxis\\ am Institut f\"ur Softwaretechnologie\\
     1.5         der Technischen Universit\"at Graz\\
     1.6         Arbeitsprotokoll}
     1.7 -\author{Thomas Leh\\
     1.8 +\author{Alexander Kargl\\
     1.9         xxx@yyy}
    1.10  \date{\today}
    1.11  
    1.12 @@ -27,10 +27,11 @@
    1.13   & Demonstration des Theorem Provers Isabelle & 0.5\\
    1.14   & Einf\"uhrung Linux, objektorientierte/funktionale Programmierung& 2.0\\
    1.15   & Installation: Isabelle, \sisac-core, Mercurial & 3.0\\ \hline
    1.16 -13.7.11 &  & \\
    1.17 - &  & \\
    1.18 - &  & \\
    1.19 - &  & \\
    1.20 +13.7.11
    1.21 + & Einf\"uhrung Latex & 1.0 \\
    1.22 + & Einf\"uhrung ML & 1.5 \\
    1.23 + & Konfiguration von Mercurial & 1.5 \\
    1.24 + & ML-Programmierung/Einführung & 3.5 \\
    1.25   &  & \\
    1.26   &  & \\
    1.27   &  & \\
     2.1 --- a/test/Tools/isac/ADDTESTS/course/ml_quickstart/ML1_Basics.thy	Wed Jul 13 10:41:17 2011 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,58 +0,0 @@
     2.4 -header {* Quick introduction to ML, session 1 *}
     2.5 -theory ML1_Basics imports Isac begin
     2.6 -
     2.7 -text{*
     2.8 -This course follows the book:
     2.9 -J.D.Ullmann, Elements of ML Programming. Prenctice Hall 1998.
    2.10 -Contents:
    2.11 -
    2.12 -section {* 2.1 Expressions .. 2.1.5*}
    2.13 -ML {*
    2.14 -~1;
    2.15 -1 - 2;
    2.16 -1.2345;
    2.17 -"1234asdf";
    2.18 -1 < 2;
    2.19 -*}
    2.20 -
    2.21 -section {* 2.1.6 If-Then-Else*}
    2.22 -ML {*
    2.23 -val i = 3; (*"val" stores the "value" 7 into the "variable" i*)
    2.24 -if 5 < i 
    2.25 -then writeln "i is greater then 5"
    2.26 -else writeln "i is not greater than 5";
    2.27 -(*
    2.28 -if 5 < i 
    2.29 -then "i is greater then 5"
    2.30 -else 5
    2.31 -*)
    2.32 -*}
    2.33 -
    2.34 -ML {*
    2.35 -if 5 < i 
    2.36 -then "i is greater then 5"
    2.37 -else "i is not greater than 5";
    2.38 -if 5 < i 
    2.39 -then 5 + 10
    2.40 -else i + 10;
    2.41 -val x = if 5 < i 
    2.42 -  then "i is greater then 5"
    2.43 -  else "i is not greater than 5";
    2.44 -*}
    2.45 -
    2.46 -section {* 2.4 Tuples and Lists *}
    2.47 -ML {*
    2.48 -val t = (4, 5.0 + 1.0, "six", 1 < 2);
    2.49 -val (a, _, _, d) = (4, 5.0 + 1.0, "six", 1 < 2); (*pattern matching*)
    2.50 -*}
    2.51 -ML {*
    2.52 -val l = [1, 2, 3, 4, 5, 6, 7];
    2.53 -1 :: (2 :: (3 :: [])); (* list constructor "::"*)
    2.54 -val l1 = 0 :: l;
    2.55 -val fi :: _ = l1;
    2.56 -*}
    2.57 -
    2.58 -section {* 3 Defining functions *}
    2.59 -text {* see src/Pure/library.ML *}
    2.60 -
    2.61 -end