equal
deleted
inserted
replaced
27 val Ex1_def = thm "Ex1_def"; |
27 val Ex1_def = thm "Ex1_def"; |
28 val iff = thm "iff"; |
28 val iff = thm "iff"; |
29 val True_or_False = thm "True_or_False"; |
29 val True_or_False = thm "True_or_False"; |
30 val Let_def = thm "Let_def"; |
30 val Let_def = thm "Let_def"; |
31 val if_def = thm "if_def"; |
31 val if_def = thm "if_def"; |
32 val arbitrary_def = thm "arbitrary_def"; |
|
33 |
32 |
34 |
33 |
35 section "Equality"; |
34 section "Equality"; |
36 |
35 |
37 Goal "s=t ==> t=s"; |
36 Goal "s=t ==> t=s"; |