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
```