Fixed Problem with ML-bindings for thm names;
authorchaieb
Thu Jun 14 09:37:38 2007 +0200 (2007-06-14)
changeset 23381da53d861d106
parent 23380 15f7a6745cce
child 23382 0459ab90389a
Fixed Problem with ML-bindings for thm names;
src/HOL/Complex/ex/mirtac.ML
     1.1 --- a/src/HOL/Complex/ex/mirtac.ML	Thu Jun 14 07:27:55 2007 +0200
     1.2 +++ b/src/HOL/Complex/ex/mirtac.ML	Thu Jun 14 09:37:38 2007 +0200
     1.3 @@ -105,14 +105,16 @@
     1.4        addsplits [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, @{thm "split_min"}, @{thm "split_max"}]
     1.5      (* Simp rules for changing (n::int) to int n *)
     1.6      val simpset1 = HOL_basic_ss
     1.7 -      addsimps [nat_number_of_def, zdvd_int] @ map (fn r => r RS sym)
     1.8 -        [int_int_eq, zle_int, zless_int, zadd_int, zmult_int]
     1.9 -      addsplits [zdiff_int_split]
    1.10 +      addsimps [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}] @ map (fn r => r RS sym)
    1.11 +        [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}, @{thm "zadd_int"}, 
    1.12 +         @{thm "zmult_int"}]
    1.13 +      addsplits [@{thm "zdiff_int_split"}]
    1.14      (*simp rules for elimination of int n*)
    1.15  
    1.16      val simpset2 = HOL_basic_ss
    1.17 -      addsimps [nat_0_le, all_nat, ex_nat, number_of1, number_of2, int_0, int_1]
    1.18 -      addcongs [conj_le_cong, imp_le_cong]
    1.19 +      addsimps [@{thm "nat_0_le"}, @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "number_of1"}, 
    1.20 +                @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}]
    1.21 +      addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
    1.22      (* simp rules for elimination of abs *)
    1.23      val ct = cterm_of sg (HOLogic.mk_Trueprop t)
    1.24      (* Theorem for the nat --> int transformation *)