equal
deleted
inserted
replaced
1 (* Title: HOL/Library/OptionalSugar.thy |
1 (* Title: HOL/Library/OptionalSugar.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Gerwin Klain, Tobias Nipkow |
3 Author: Gerwin Klain, Tobias Nipkow |
4 Copyright 2005 NICTA and TUM |
4 Copyright 2005 NICTA and TUM |
5 *) |
5 *) |
6 |
6 (*<*) |
7 theory OptionalSugar |
7 theory OptionalSugar |
8 imports LaTeXsugar |
8 imports LaTeXsugar |
9 begin |
9 begin |
10 |
10 |
11 (* append *) |
11 (* append *) |
33 "_bind (p#DUMMY) e" <= "_bind p (hd e)" |
33 "_bind (p#DUMMY) e" <= "_bind p (hd e)" |
34 "_bind (DUMMY#p) e" <= "_bind p (tl e)" |
34 "_bind (DUMMY#p) e" <= "_bind p (tl e)" |
35 |
35 |
36 |
36 |
37 end |
37 end |
|
38 (*>*) |