removed obsolete old-style cs/css;
authorwenzelm
Thu May 12 22:37:31 2011 +0200 (2011-05-12)
changeset 4277329042b3e7575
parent 42772 2acb503fd857
child 42774 6c999448c2bb
removed obsolete old-style cs/css;
src/HOL/TLA/TLA.thy
     1.1 --- a/src/HOL/TLA/TLA.thy	Thu May 12 22:35:15 2011 +0200
     1.2 +++ b/src/HOL/TLA/TLA.thy	Thu May 12 22:37:31 2011 +0200
     1.3 @@ -138,10 +138,6 @@
     1.4  
     1.5  declare tempI [intro!]
     1.6  declare tempD [dest]
     1.7 -ML {*
     1.8 -val temp_css = (@{claset}, @{simpset})
     1.9 -val temp_cs = op addss temp_css
    1.10 -*}
    1.11  
    1.12  (* Modify the functions that add rules to simpsets, classical sets,
    1.13     and clasimpsets in order to accept "lifted" theorems
    1.14 @@ -427,12 +423,6 @@
    1.15  
    1.16  lemmas temp_simps [temp_rewrite, simp] = BoxConst DmdConst
    1.17  
    1.18 -(* Make these rewrites active by default *)
    1.19 -ML {*
    1.20 -val temp_css = temp_css addsimps2 @{thms temp_simps}
    1.21 -val temp_cs = op addss temp_css
    1.22 -*}
    1.23 -
    1.24  
    1.25  (* ------------------------ Further rewrites ----------------------------------------- *)
    1.26  section "Further rewrites"