equal
deleted
inserted
replaced
100 apply(blast) |
100 apply(blast) |
101 done |
101 done |
102 |
102 |
103 theorem "mc f = {s. s \<Turnstile> f}"; |
103 theorem "mc f = {s. s \<Turnstile> f}"; |
104 apply(induct_tac f); |
104 apply(induct_tac f); |
105 apply(auto simp add:EF_lemma); |
105 apply(auto simp add: EF_lemma); |
106 done; |
106 done; |
107 |
107 |
108 text{* |
108 text{* |
109 \begin{exercise} |
109 \begin{exercise} |
110 @{term AX} has a dual operator @{term EN}\footnote{We cannot use the customary @{text EX} |
110 @{term AX} has a dual operator @{term EN}\footnote{We cannot use the customary @{text EX} |