author | wenzelm |
Tue, 03 Oct 2000 01:14:52 +0200 | |
changeset 10131 | 546686f0a6fb |
parent 9895 | 75e55370b1ae |
child 10276 | 75e2c6cb4153 |
permissions | -rw-r--r-- |
(* Title: HOL/subset.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge *) theory subset = Set files "Tools/typedef_package.ML": (*belongs to theory Ord*) theorems linorder_cases [case_names less equal greater] = linorder_less_split (*belongs to theory Set*) setup Rulify.setup end