changeset 168 | 44ff2275d44f |
parent 156 | fd1be45b64bf |
child 171 | 16c4ea954511 |
--- a/IOA/meta_theory/Option.ML Wed Nov 09 19:50:36 1994 +0100 +++ b/IOA/meta_theory/Option.ML Wed Nov 09 19:51:09 1994 +0100 @@ -1,3 +1,11 @@ +(* Title: Option.ML + ID: $Id$ + Author: Tobias Nipkow + Copyright 1994 TU Muenchen + +Derived rules +*) + val option_rws = Let_def :: Option.option.simps; val SS = arith_ss addsimps option_rws;