src/ZF/ex/Enum.ML
author wenzelm
Sun, 25 Oct 1998 12:33:27 +0100
changeset 5769 6a422b22ba02
parent 5068 fb28eaa07e01
child 6141 a6922171b396
permissions -rw-r--r--
tuned checklist;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 515
diff changeset
     1
(*  Title:      ZF/ex/Enum
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 515
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Example of a BIG enumeration type
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
56
2caa6f49f06e ZF/ex/tf/tree,forest_unfold: streamlined the proofs
lcp
parents: 38
diff changeset
     8
Can go up to at least 100 constructors, but it takes nearly 7 minutes...
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
515
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    11
open Enum;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4091
diff changeset
    13
Goal "C00 ~= C01";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 2469
diff changeset
    14
by (simp_tac (simpset() addsimps enum.free_iffs) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16