equal
deleted
inserted
replaced
1 (* Title: Admin/Benchmarks/HOL-datatype/Brackin.thy |
1 (* Title: Admin/Benchmarks/HOL-datatype/Brackin.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 *) |
3 *) |
4 |
4 |
5 theory Brackin = Main: |
5 theory Brackin imports Main begin |
6 |
6 |
7 (* ------------------------------------------------------------------------- *) |
7 (* ------------------------------------------------------------------------- *) |
8 (* A couple from Steve Brackin's work. *) |
8 (* A couple from Steve Brackin's work. *) |
9 (* ------------------------------------------------------------------------- *) |
9 (* ------------------------------------------------------------------------- *) |
10 |
10 |