# HG changeset patch # User haftmann # Date 1162560156 -3600 # Node ID 405ebd7ba8816bf87dc3efa83a5c8add199abf49 # Parent ee207b9b8bf588c72784acd7937a27c5cd9aebb9 dropped prop_cs diff -r ee207b9b8bf5 -r 405ebd7ba881 src/HOL/HOL.ML --- a/src/HOL/HOL.ML Fri Nov 03 14:22:35 2006 +0100 +++ b/src/HOL/HOL.ML Fri Nov 03 14:22:36 2006 +0100 @@ -1,6 +1,5 @@ (* legacy ML bindings *) -val prop_cs = HOL.claset_prop; val HOL_cs = HOL.claset; val HOL_basic_ss = HOL.simpset_basic; val HOL_ss = HOL.simpset;