src/sml/Scripts/Script.thy
changeset 2918 cac1f942e1a1
parent 1330 1d7b3872e940
child 3758 6d7bf1d2f94d
equal deleted inserted replaced
2917:2488337fd0dd 2918:cac1f942e1a1
    27 
    27 
    28 (*tactics*)
    28 (*tactics*)
    29   Rewrite      :: "[ID, bool, 'a] => 'a"
    29   Rewrite      :: "[ID, bool, 'a] => 'a"
    30   Rewrite'_Inst:: "[(real * real) list, ID, bool, 'a] => 'a"
    30   Rewrite'_Inst:: "[(real * real) list, ID, bool, 'a] => 'a"
    31 			             ("(Rewrite'_Inst (_ _ _))" 11)
    31 			             ("(Rewrite'_Inst (_ _ _))" 11)
    32                                      (*without last argument ^^ FIXXXXME*)
    32                                      (*without last argument ^^ for @@*)
    33   Rewrite'_Set :: "[ID, bool, 'a] => 'a" ("(Rewrite'_Set (_ _))" 11)
    33   Rewrite'_Set :: "[ID, bool, 'a] => 'a" ("(Rewrite'_Set (_ _))" 11)
    34   Rewrite'_Set'_Inst
    34   Rewrite'_Set'_Inst
    35                :: "[(real * real) list, ID, bool, 'a] => 'a"
    35                :: "[(real * real) list, ID, bool, 'a] => 'a"
    36 		                     ("(Rewrite'_Set'_Inst (_ _ _))" 11)
    36 		                     ("(Rewrite'_Set'_Inst (_ _ _))" 11)
    37                                      (*without last argument ^^ FIXXXXME*)
    37                                      (*without last argument ^^ for @@*)
    38   Calculate    :: "[ID, 'a] => 'a"
    38   Calculate    :: "[ID, 'a] => 'a"
    39   Substitute   :: "[(real * real) list, 'a] => 'a"
    39   Substitute   :: "[(real * real) list, 'a] => 'a"
    40   Map          :: "['a => 'b, 'a list] => 'b list"
    40   Map          :: "['a => 'b, 'a list] => 'b list"
    41   Tac        :: "ID => 'a"
    41   Tac          :: "ID => 'a"         (*deprecated; only use in Test.ML*)
    42   Check'_elementwise ::
    42   Check'_elementwise ::
    43 		  "['a list, 'b set] => 'a list"
    43 		  "['a list, 'b set] => 'a list"
    44                                      ("Check'_elementwise (_ _)" 11)
    44                                      ("Check'_elementwise (_ _)" 11)
    45   Assumptions  :: bool
    45   Assumptions  :: bool
    46   SubProblem   :: "[ID * ID list * ID list, arg list] => 'a"
    46   SubProblem   :: "[ID * ID list * ID list, arg list] => 'a"