src/Pure/deriv.ML
changeset 6085 3d8dcb09dbfb
parent 2672 85d7e800d754
equal deleted inserted replaced
6084:842b059e023f 6085:3d8dcb09dbfb
    11   (*Object-level rules*)
    11   (*Object-level rules*)
    12   datatype orule = Subgoal of cterm
    12   datatype orule = Subgoal of cterm
    13 		 | Asm of int
    13 		 | Asm of int
    14 		 | Res of deriv
    14 		 | Res of deriv
    15 		 | Equal of deriv
    15 		 | Equal of deriv
    16 		 | Thm   of string
    16 		 | Thm   of string * tag list
    17 		 | Other of deriv;
    17 		 | Other of deriv;
    18 
    18 
    19   val size : deriv -> int
    19   val size : deriv -> int
    20   val drop : 'a mtree * int -> 'a mtree
    20   val drop : 'a mtree * int -> 'a mtree
    21   val linear : deriv -> deriv list
    21   val linear : deriv -> deriv list
    47 (*Object-level rules*)
    47 (*Object-level rules*)
    48 datatype orule = Subgoal of cterm
    48 datatype orule = Subgoal of cterm
    49 	       | Asm of int
    49 	       | Asm of int
    50                | Res of deriv
    50                | Res of deriv
    51                | Equal of deriv
    51                | Equal of deriv
    52                | Thm   of string
    52                | Thm   of string * tag list
    53                | Other of deriv;
    53                | Other of deriv;
    54 
    54 
    55 (*At position i, splice in value x, removing ngoal elements*)
    55 (*At position i, splice in value x, removing ngoal elements*)
    56 fun splice (i,x,ngoal,prfs) =
    56 fun splice (i,x,ngoal,prfs) =
    57     let val prfs0 = take(i-1,prfs)
    57     let val prfs0 = take(i-1,prfs)