src/ZF/ex/Enum.ML
author mueller
Thu, 17 Jul 1997 12:44:58 +0200
changeset 3523 23eae933c2d9
parent 2469 b50b8c0eec01
child 4091 771b1f6422a8
permissions -rw-r--r--
changes needed for introducing fairness
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
515
abcc438e7c27 installation of new inductive/datatype sections
lcp
parents: 477
diff changeset
    13
goal Enum.thy "C00 ~= C01";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
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