equal
deleted
inserted
replaced
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1998 TUM |
4 Copyright 1998 TUM |
5 *) |
5 *) |
6 |
6 |
7 AutoMaxChop = DA + MaxChop + |
7 theory AutoMaxChop = DA + MaxChop: |
8 |
8 |
9 consts |
9 consts |
10 auto_split :: "('a,'s)da => 's => 'a list * 'a list => 'a list => 'a splitter" |
10 auto_split :: "('a,'s)da => 's => 'a list * 'a list => 'a list => 'a splitter" |
11 primrec |
11 primrec |
12 "auto_split A q res ps [] = (if fin A q then (ps,[]) else res)" |
12 "auto_split A q res ps [] = (if fin A q then (ps,[]) else res)" |