# HG changeset patch
# User wenzelm
# Date 1305232651 -7200
# Node ID 29042b3e7575922d0ad8afd93326049c2f2d7374
# Parent  2acb503fd857de3b2e97f938415aaea3bf6c4e71
removed obsolete old-style cs/css;

diff -r 2acb503fd857 -r 29042b3e7575 src/HOL/TLA/TLA.thy
--- a/src/HOL/TLA/TLA.thy	Thu May 12 22:35:15 2011 +0200
+++ b/src/HOL/TLA/TLA.thy	Thu May 12 22:37:31 2011 +0200
@@ -138,10 +138,6 @@
 
 declare tempI [intro!]
 declare tempD [dest]
-ML {*
-val temp_css = (@{claset}, @{simpset})
-val temp_cs = op addss temp_css
-*}
 
 (* Modify the functions that add rules to simpsets, classical sets,
    and clasimpsets in order to accept "lifted" theorems
@@ -427,12 +423,6 @@
 
 lemmas temp_simps [temp_rewrite, simp] = BoxConst DmdConst
 
-(* Make these rewrites active by default *)
-ML {*
-val temp_css = temp_css addsimps2 @{thms temp_simps}
-val temp_cs = op addss temp_css
-*}
-
 
 (* ------------------------ Further rewrites ----------------------------------------- *)
 section "Further rewrites"