isabelle: src/HOL/subset.thy@cc2340c338f0 (annotated)

1475 7f5a4cd08209 expanded tabs; renamed subtype to typedef; clasohm parents: 923 diff changeset	1	(* Title: HOL/subset.thy
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	2	ID: $Id$
1475 7f5a4cd08209 expanded tabs; renamed subtype to typedef; clasohm parents: 923 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
923 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
7705 222b715b5d24 Tools/typedef_package.ML; wenzelm parents: 5853 diff changeset	7	theory subset = Set
222b715b5d24 Tools/typedef_package.ML; wenzelm parents: 5853 diff changeset	8	files "Tools/typedef_package.ML":
222b715b5d24 Tools/typedef_package.ML; wenzelm parents: 5853 diff changeset	9
7717 e7ecfa617443 Added attribute rulify_prems (useful for modifying premises of introduction berghofe parents: 7705 diff changeset	10	setup rulify_prems_attrib_setup
e7ecfa617443 Added attribute rulify_prems (useful for modifying premises of introduction berghofe parents: 7705 diff changeset	11
7705 222b715b5d24 Tools/typedef_package.ML; wenzelm parents: 5853 diff changeset	12	end