diff options
| -rw-r--r-- | isa/Example-Xsym.ML | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/isa/Example-Xsym.ML b/isa/Example-Xsym.ML index 46f93938..d566a850 100644 --- a/isa/Example-Xsym.ML +++ b/isa/Example-Xsym.ML @@ -6,7 +6,7 @@ Just a version of Example.ML using XSymbol *) -Goal "A \\<and> B \\<longrightarrow> B \\<and> A"; +Goal "A \\<and> B \\<longrightarrow> B \\<and> A"; by (rtac impI 1); by (etac conjE 1); by (rtac conjI 1); |