src/HOL/Finite.thy
author clasohm
Wed, 29 Nov 1995 16:44:59 +0100
changeset 1370 7361ac9b024d
parent 923 ff1574a81019
child 1475 7f5a4cd08209
permissions -rw-r--r--
removed quotes from types in consts and syntax sections
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     1
(*  Title: 	HOL/Finite.thy
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     5
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     6
Finite powerset operator
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     7
*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     8
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     9
Finite = Lfp +
1370
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 923
diff changeset
    10
consts Fin :: 'a set => 'a set set
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    11
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    12
inductive "Fin(A)"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    13
  intrs
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    14
    emptyI  "{} : Fin(A)"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    15
    insertI "[| a: A;  b: Fin(A) |] ==> insert a b : Fin(A)"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    16
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    17
end