equal
deleted
inserted
replaced
1 (* Title: HOL/Import/MakeEqual.thy |
1 (* Title: HOL/Import/MakeEqual.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Sebastian Skalberg (TU Muenchen) |
3 Author: Sebastian Skalberg (TU Muenchen) |
4 *) |
4 *) |
5 |
5 |
6 theory MakeEqual = Main |
6 theory MakeEqual imports Main |
7 files "shuffler.ML": |
7 uses "shuffler.ML" begin |
8 |
8 |
9 setup Shuffler.setup |
9 setup Shuffler.setup |
10 |
10 |
11 lemma conj_norm [shuffle_rule]: "(A & B ==> PROP C) == ([| A ; B |] ==> PROP C)" |
11 lemma conj_norm [shuffle_rule]: "(A & B ==> PROP C) == ([| A ; B |] ==> PROP C)" |
12 proof |
12 proof |