author | wenzelm |
Tue, 12 Jan 1999 12:29:50 +0100 | |
changeset 6085 | 3d8dcb09dbfb |
parent 6084 | 842b059e023f |
child 6086 | 8cd4190e633a |
src/Pure/deriv.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/deriv.ML Tue Jan 12 12:29:24 1999 +0100 +++ b/src/Pure/deriv.ML Tue Jan 12 12:29:50 1999 +0100 @@ -13,7 +13,7 @@ | Asm of int | Res of deriv | Equal of deriv - | Thm of string + | Thm of string * tag list | Other of deriv; val size : deriv -> int @@ -49,7 +49,7 @@ | Asm of int | Res of deriv | Equal of deriv - | Thm of string + | Thm of string * tag list | Other of deriv; (*At position i, splice in value x, removing ngoal elements*)