added Combinators in test/Pure/General/Basics.thy decompose-isar
authorAlexander Kargl <akargl@brgkepler.net>
Fri, 15 Jul 2011 09:09:18 +0200
branchdecompose-isar
changeset 4208783632832775e
parent 42086 bfd0e5822ea4
child 42089 d949bb8c415b
added Combinators in test/Pure/General/Basics.thy
doc-src/isac/akargl/ferialprakt.tex
test/Pure/General/Basics.thy
     1.1 --- a/doc-src/isac/akargl/ferialprakt.tex	Thu Jul 14 14:36:01 2011 +0200
     1.2 +++ b/doc-src/isac/akargl/ferialprakt.tex	Fri Jul 15 09:09:18 2011 +0200
     1.3 @@ -22,20 +22,21 @@
     1.4  \begin{center}
     1.5  \begin{tabular}{l|l|r}
     1.6  Datum   & T\"atigkeit & Std. \\ \hline
     1.7 -12.7.11
     1.8 +12.7.2011
     1.9   & Demonstration des ``educational math assistant \sisac'' & 1.0\\
    1.10   & Demonstration des Theorem Provers Isabelle & 0.5\\
    1.11   & Einf\"uhrung Linux, objektorientierte/funktionale Programmierung& 2.0\\
    1.12   & Installation: Isabelle, \sisac-core, Mercurial & 3.0\\ \hline
    1.13 -13.7.11
    1.14 +13.7.2011
    1.15   & Einf\"uhrung Latex & 1.0 \\
    1.16   & Einf\"uhrung ML & 1.5 \\
    1.17   & Konfiguration von Mercurial & 1.5 \\
    1.18 - & ML-Programmierung/Einführung & 3.5 \\
    1.19 - &  & \\
    1.20 - &  & \\
    1.21 - &  & \\
    1.22 - &  & \\
    1.23 + & ML-Programmierung/Einf\"uhrung & 3.5 \\ \hline
    1.24 +14.7.2011
    1.25 + & Einf\"uhrung ML & 1.5 \\
    1.26 + & Programmierung ML & 2 \\
    1.27 + & Einf\"uhrung ML II & 1 \\
    1.28 + & Erstellung v. Beispielen f\"ur Kombinatoren in ML & 3 \\
    1.29   &  & \\
    1.30   &  & \\
    1.31  \end{tabular}
     2.1 --- a/test/Pure/General/Basics.thy	Thu Jul 14 14:36:01 2011 +0200
     2.2 +++ b/test/Pure/General/Basics.thy	Fri Jul 15 09:09:18 2011 +0200
     2.3 @@ -30,5 +30,45 @@
     2.4  (*val it = ("a", 11) : string * int*)
     2.5  *}
     2.6  
     2.7 +ML {*
     2.8 +  op ||>>;
     2.9 +  (444, 2) ||>> (fn e => (e * 3, e + 5));
    2.10 +  (*val it = ((7, 2), 4): (int * int) * int*)
    2.11 +*}
    2.12 +
    2.13 +ML {*
    2.14 +  op #>;
    2.15 +  ((fn a => a + 10) #> (fn a => a + 5)) 3;
    2.16 +  (*val it = 18: int*)
    2.17 +*}
    2.18 +
    2.19 +ML {*
    2.20 +  op #->;
    2.21 +  fun ff c a = a + c;
    2.22 +  ((fn e => (e * 2, e + 99))  #-> ff) 50;
    2.23 +  (*val it = 249: int*)
    2.24 +*}
    2.25 +
    2.26 +ML {*
    2.27 +  op #>>;
    2.28 +  fun fff a = (a + 10, string_of_int a);
    2.29 +  fun ggg b = b * 2;
    2.30 +  fff #>> ggg;
    2.31 +  (fff #>> ggg) 1;
    2.32 +  (*val it = (22, "1"): int * string*)
    2.33 +*}
    2.34 +
    2.35 +ML {*
    2.36 +  op ##>;
    2.37 +  ((fn e => (e * 3, e + 4)) ##> (fn a => a + 5)) 6;
    2.38 +  (*val it = (18, 15): int * int*)
    2.39 +*}
    2.40 +
    2.41 +ML {*
    2.42 +  op ##>>;
    2.43 +  ((fn e => (e * 2, e + 3)) ##>> (fn u => (u * 4, u + 5))) 6;
    2.44 +  (*val it = ((12, 36), 14): (int * int) * int*)
    2.45 +*}
    2.46 +
    2.47  end
    2.48