equal
deleted
inserted
replaced
28 val exI = thm "exI"; |
28 val exI = thm "exI"; |
29 val exE = thm "exE"; |
29 val exE = thm "exE"; |
30 val eq_reflection = thm "eq_reflection"; |
30 val eq_reflection = thm "eq_reflection"; |
31 val iff_reflection = thm "iff_reflection"; |
31 val iff_reflection = thm "iff_reflection"; |
32 |
32 |
|
33 structure IFOL = |
|
34 struct |
|
35 val thy = the_context (); |
|
36 val refl = refl; |
|
37 val subst = subst; |
|
38 val conjI = conjI; |
|
39 val conjunct1 = conjunct1; |
|
40 val conjunct2 = conjunct2; |
|
41 val disjI1 = disjI1; |
|
42 val disjI2 = disjI2; |
|
43 val disjE = disjE; |
|
44 val impI = impI; |
|
45 val mp = mp; |
|
46 val FalseE = FalseE; |
|
47 val True_def = True_def; |
|
48 val not_def = not_def; |
|
49 val iff_def = iff_def; |
|
50 val ex1_def = ex1_def; |
|
51 val allI = allI; |
|
52 val spec = spec; |
|
53 val exI = exI; |
|
54 val exE = exE; |
|
55 val eq_reflection = eq_reflection; |
|
56 val iff_reflection = iff_reflection; |
|
57 end; |
33 |
58 |
34 |
59 |
35 Goalw [True_def] "True"; |
60 Goalw [True_def] "True"; |
36 by (REPEAT (ares_tac [impI] 1)) ; |
61 by (REPEAT (ares_tac [impI] 1)) ; |
37 qed "TrueI"; |
62 qed "TrueI"; |