src/ZF/simpdata.ML
changeset 38513 33ab01218ae1
parent 36543 0e7fc5bf38de
child 38715 6513ea67d95d
     1.1 --- a/src/ZF/simpdata.ML	Wed Aug 18 11:55:27 2010 +0200
     1.2 +++ b/src/ZF/simpdata.ML	Wed Aug 18 12:08:21 2010 +0200
     1.3 @@ -19,27 +19,27 @@
     1.4                     | NONE => [th])
     1.5              | _ => [th]
     1.6    in case concl_of th of
     1.7 -         Const("Trueprop",_) $ P =>
     1.8 +         Const(@{const_name Trueprop},_) $ P =>
     1.9              (case P of
    1.10                   Const(@{const_name mem},_) $ a $ b => tryrules mem_pairs b
    1.11 -               | Const("True",_)         => []
    1.12 -               | Const("False",_)        => []
    1.13 +               | Const(@{const_name True},_)         => []
    1.14 +               | Const(@{const_name False},_)        => []
    1.15                 | A => tryrules conn_pairs A)
    1.16         | _                       => [th]
    1.17    end;
    1.18  
    1.19  (*Analyse a rigid formula*)
    1.20  val ZF_conn_pairs =
    1.21 -  [("Ball",     [@{thm bspec}]),
    1.22 -   ("All",      [@{thm spec}]),
    1.23 -   ("op -->",   [@{thm mp}]),
    1.24 -   ("op &",     [@{thm conjunct1}, @{thm conjunct2}])];
    1.25 +  [(@{const_name Ball}, [@{thm bspec}]),
    1.26 +   (@{const_name All}, [@{thm spec}]),
    1.27 +   (@{const_name "op -->"}, [@{thm mp}]),
    1.28 +   (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}])];
    1.29  
    1.30  (*Analyse a:b, where b is rigid*)
    1.31  val ZF_mem_pairs =
    1.32 -  [("Collect",  [@{thm CollectD1}, @{thm CollectD2}]),
    1.33 -   (@{const_name Diff},     [@{thm DiffD1}, @{thm DiffD2}]),
    1.34 -   (@{const_name Int},   [@{thm IntD1}, @{thm IntD2}])];
    1.35 +  [(@{const_name Collect}, [@{thm CollectD1}, @{thm CollectD2}]),
    1.36 +   (@{const_name Diff}, [@{thm DiffD1}, @{thm DiffD2}]),
    1.37 +   (@{const_name Int}, [@{thm IntD1}, @{thm IntD2}])];
    1.38  
    1.39  val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
    1.40