Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
TFL/examples/Subst/NNF.ML
author paulson
Fri, 14 Feb 1997 10:38:48 +0100
changeset 2615 99df9182f5a5
parent 2113 21266526ac42
permissions -rw-r--r--
Tidying and a corrected comment
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2113
21266526ac42 Subst as modified by Konrad Slind
paulson
parents:
diff changeset 
     1
 
goal HOL.thy "(~(!x. P x)) = (? x. ~(P x)) & \
21266526ac42 Subst as modified by Konrad Slind
paulson
parents:
diff changeset 
     2
 
           \  (~(? x. P x)) = (!x. ~(P x)) & \
21266526ac42 Subst as modified by Konrad Slind
paulson
parents:
diff changeset 
     3
 
           \  (~(x-->y)) = (x & (~ y))     & \
21266526ac42 Subst as modified by Konrad Slind
paulson
parents:
diff changeset 
     4
 
           \  ((~ x) | y) = (x --> y)      & \
21266526ac42 Subst as modified by Konrad Slind
paulson
parents:
diff changeset 
     5
 
           \  (~(x & y)) = ((~ x) | (~ y)) & \
21266526ac42 Subst as modified by Konrad Slind
paulson
parents:
diff changeset 
     6
 
           \  (~(x | y)) = ((~ x) & (~ y)) & \
21266526ac42 Subst as modified by Konrad Slind
paulson
parents:
diff changeset 
     7
 
           \  (~(~x)) = x";
21266526ac42 Subst as modified by Konrad Slind
paulson
parents:
diff changeset 
     8
 
by (fast_tac HOL_cs 1);
21266526ac42 Subst as modified by Konrad Slind
paulson
parents:
diff changeset 
     9
 
val NNF_rews = map (fn th => th RS eq_reflection)
21266526ac42 Subst as modified by Konrad Slind
paulson
parents:
diff changeset 
    10
 
                   (Prim.Rules.CONJUNCTS (result()))
21266526ac42 Subst as modified by Konrad Slind
paulson
parents:
diff changeset 
    11
 














isabelle