author | nipkow |
Thu, 12 Oct 2000 13:01:19 +0200 | |
changeset 10202 | 9e8b4bebc940 |
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