Admin/Benchmarks/HOL-datatype/Brackin.thy
changeset 16417 9bc16273c2d4
parent 7373 776d888472aa
child 33695 bec342db1bf4
equal deleted inserted replaced
16416:6061ae1f90f2 16417:9bc16273c2d4
     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