isabelle: src/HOL/subset.thy@4961c73b5f60 (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
9895 75e55370b1ae added linorder_cases; wenzelm parents: 7717 diff changeset	10	(belongs to theory Ord)
75e55370b1ae added linorder_cases; wenzelm parents: 7717 diff changeset	11	theorems linorder_cases [case_names less equal greater] =
75e55370b1ae added linorder_cases; wenzelm parents: 7717 diff changeset	12	linorder_less_split
75e55370b1ae added linorder_cases; wenzelm parents: 7717 diff changeset	13
75e55370b1ae added linorder_cases; wenzelm parents: 7717 diff changeset	14	(belongs to theory Set)
75e55370b1ae added linorder_cases; wenzelm parents: 7717 diff changeset	15	setup Rulify.setup
7717 e7ecfa617443 Added attribute rulify_prems (useful for modifying premises of introduction berghofe parents: 7705 diff changeset	16
7705 222b715b5d24 Tools/typedef_package.ML; wenzelm parents: 5853 diff changeset	17	end

author	wenzelm
	Sun, 17 Sep 2000 22:25:18 +0200
changeset 10012	4961c73b5f60
parent 9895	75e55370b1ae
child 10276	75e2c6cb4153
permissions	-rw-r--r--