src/FOLP/ex/Classical.thy
changeset 58860 fee7cfa69c50
parent 36319 8feb2c4bef1a
child 58957 c9e744ea8a38
     1.1 --- a/src/FOLP/ex/Classical.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/FOLP/ex/Classical.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -145,7 +145,7 @@
     1.4    by (tactic "fast_tac FOLP_cs 1")
     1.5  
     1.6  text "Problem 21"
     1.7 -schematic_lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))";
     1.8 +schematic_lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))"
     1.9    by (tactic "best_tac FOLP_dup_cs 1")
    1.10  
    1.11  text "Problem 22"
    1.12 @@ -173,7 +173,7 @@
    1.13  text "Problem 26"
    1.14  schematic_lemma "?u : ((EX x. p(x)) <-> (EX x. q(x))) &   
    1.15       (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))   
    1.16 -  --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))";
    1.17 +  --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))"
    1.18    by (tactic "fast_tac FOLP_cs 1")
    1.19  
    1.20  text "Problem 27"