src/FOL/ex/Miniscope.thy

 begin
 
 
 lemmas ccontr = FalseE [THEN classical]
 
-subsection {* Negation Normal Form *}
+subsection \<open>Negation Normal Form\<close>
 
-subsubsection {* de Morgan laws *}
+subsubsection \<open>de Morgan laws\<close>
 
 lemma demorgans:
   "~(P&Q) <-> ~P | ~Q"
   "~(P|Q) <-> ~P & ~Q"
   "~~P <-> P"

   by blast+
 
 
 (* BEWARE: rewrite rules for <-> can confuse the simplifier!! *)
 
-subsubsection {* Pushing in the existential quantifiers *}
+subsubsection \<open>Pushing in the existential quantifiers\<close>
 
 lemma ex_simps:
   "(EX x. P) <-> P"
   "!!P Q. (EX x. P(x) & Q) <-> (EX x. P(x)) & Q"
   "!!P Q. (EX x. P & Q(x)) <-> P & (EX x. Q(x))"

   "!!P Q. (EX x. P(x) | Q) <-> (EX x. P(x)) | Q"
   "!!P Q. (EX x. P | Q(x)) <-> P | (EX x. Q(x))"
   by blast+
 
 
-subsubsection {* Pushing in the universal quantifiers *}
+subsubsection \<open>Pushing in the universal quantifiers\<close>
 
 lemma all_simps:
   "(ALL x. P) <-> P"
   "!!P Q. (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))"
   "!!P Q. (ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q"

   "!!P Q. (ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"
   by blast+
 
 lemmas mini_simps = demorgans nnf_simps ex_simps all_simps
 
-ML {*
+ML \<open>
 val mini_ss = simpset_of (@{context} addsimps @{thms mini_simps});
 fun mini_tac ctxt =
   resolve_tac ctxt @{thms ccontr} THEN' asm_full_simp_tac (put_simpset mini_ss ctxt);
-*}
+\<close>
 
 end