src/sml/Scripts/Script.thy
changeset 2918 cac1f942e1a1
parent 1330 1d7b3872e940
child 3758 6d7bf1d2f94d
     1.1 --- a/src/sml/Scripts/Script.thy	Sat Aug 20 19:10:30 2005 +0200
     1.2 +++ b/src/sml/Scripts/Script.thy	Sat Aug 20 21:20:16 2005 +0200
     1.3 @@ -29,16 +29,16 @@
     1.4    Rewrite      :: "[ID, bool, 'a] => 'a"
     1.5    Rewrite'_Inst:: "[(real * real) list, ID, bool, 'a] => 'a"
     1.6  			             ("(Rewrite'_Inst (_ _ _))" 11)
     1.7 -                                     (*without last argument ^^ FIXXXXME*)
     1.8 +                                     (*without last argument ^^ for @@*)
     1.9    Rewrite'_Set :: "[ID, bool, 'a] => 'a" ("(Rewrite'_Set (_ _))" 11)
    1.10    Rewrite'_Set'_Inst
    1.11                 :: "[(real * real) list, ID, bool, 'a] => 'a"
    1.12  		                     ("(Rewrite'_Set'_Inst (_ _ _))" 11)
    1.13 -                                     (*without last argument ^^ FIXXXXME*)
    1.14 +                                     (*without last argument ^^ for @@*)
    1.15    Calculate    :: "[ID, 'a] => 'a"
    1.16    Substitute   :: "[(real * real) list, 'a] => 'a"
    1.17    Map          :: "['a => 'b, 'a list] => 'b list"
    1.18 -  Tac        :: "ID => 'a"
    1.19 +  Tac          :: "ID => 'a"         (*deprecated; only use in Test.ML*)
    1.20    Check'_elementwise ::
    1.21  		  "['a list, 'b set] => 'a list"
    1.22                                       ("Check'_elementwise (_ _)" 11)