src/HOL/MetisExamples/Message.thy
changeset 32685 29e4e567b5f4
parent 28592 824f8390aaa2
child 32864 a226f29d4bdc
     1.1 --- a/src/HOL/MetisExamples/Message.thy	Sat Sep 19 07:38:11 2009 +0200
     1.2 +++ b/src/HOL/MetisExamples/Message.thy	Mon Sep 21 11:01:39 2009 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/MetisTest/Message.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7  
     1.8  Testing the metis method
     1.9 @@ -711,17 +710,17 @@
    1.10  proof (neg_clausify)
    1.11  assume 0: "analz (synth H) \<noteq> analz H \<union> synth H"
    1.12  have 1: "\<And>X1 X3. sup (analz (sup X3 X1)) (synth X3) = analz (sup (synth X3) X1)"
    1.13 -  by (metis analz_synth_Un sup_set_eq sup_set_eq sup_set_eq)
    1.14 +  by (metis analz_synth_Un)
    1.15  have 2: "sup (analz H) (synth H) \<noteq> analz (synth H)"
    1.16 -  by (metis 0 sup_set_eq)
    1.17 +  by (metis 0)
    1.18  have 3: "\<And>X1 X3. sup (synth X3) (analz (sup X3 X1)) = analz (sup (synth X3) X1)"
    1.19 -  by (metis 1 Un_commute sup_set_eq sup_set_eq)
    1.20 +  by (metis 1 Un_commute)
    1.21  have 4: "\<And>X3. sup (synth X3) (analz X3) = analz (sup (synth X3) {})"
    1.22 -  by (metis 3 Un_empty_right sup_set_eq)
    1.23 +  by (metis 3 Un_empty_right)
    1.24  have 5: "\<And>X3. sup (synth X3) (analz X3) = analz (synth X3)"
    1.25 -  by (metis 4 Un_empty_right sup_set_eq)
    1.26 +  by (metis 4 Un_empty_right)
    1.27  have 6: "\<And>X3. sup (analz X3) (synth X3) = analz (synth X3)"
    1.28 -  by (metis 5 Un_commute sup_set_eq sup_set_eq)
    1.29 +  by (metis 5 Un_commute)
    1.30  show "False"
    1.31    by (metis 2 6)
    1.32  qed