summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Tue, 23 May 2000 12:36:36 +0200 | |

changeset 8933 | de96f2982d2c |

parent 8932 | c1d0f7495714 |

child 8934 | 39d0cc787d47 |

theory file NatSum.thy no longer needed

src/HOL/ex/NatSum.thy | file | annotate | diff | comparison | revisions | |

src/HOL/ex/ROOT.ML | file | annotate | diff | comparison | revisions |

--- a/src/HOL/ex/NatSum.thy Tue May 23 12:35:57 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,15 +0,0 @@ -(* Title: HOL/ex/NatSum.thy - ID: $Id$ - Author: Tobias Nipkow - Copyright 1994 TU Muenchen - -A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n. -*) - -NatSum = Main + -consts sum :: [nat=>nat, nat] => nat -primrec - sum_0 "sum f 0 = 0" - sum_Suc "sum f (Suc n) = f(n) + sum f n" - -end

--- a/src/HOL/ex/ROOT.ML Tue May 23 12:35:57 2000 +0200 +++ b/src/HOL/ex/ROOT.ML Tue May 23 12:36:36 2000 +0200 @@ -17,7 +17,7 @@ with_path "../Induct" use_thy "Factorization"; time_use_thy "Primrec"; -time_use_thy "NatSum"; +time_use "NatSum"; time_use "cla.ML"; time_use "meson.ML"; time_use "mesontest.ML";