src/HOL/Main.thy
changeset 60758 d8d85a8172b5
parent 60036 218fcc645d22
child 61955 e96292f32c3c
     1.1 --- a/src/HOL/Main.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/Main.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -1,15 +1,15 @@
     1.4 -section {* Main HOL *}
     1.5 +section \<open>Main HOL\<close>
     1.6  
     1.7  theory Main
     1.8  imports Predicate_Compile Quickcheck_Narrowing Extraction Coinduction Nitpick BNF_Greatest_Fixpoint Filter
     1.9  begin
    1.10  
    1.11 -text {*
    1.12 +text \<open>
    1.13    Classical Higher-order Logic -- only ``Main'', excluding real and
    1.14    complex numbers etc.
    1.15 -*}
    1.16 +\<close>
    1.17  
    1.18 -text {* See further @{cite "Nipkow-et-al:2002:tutorial"} *}
    1.19 +text \<open>See further @{cite "Nipkow-et-al:2002:tutorial"}\<close>
    1.20  
    1.21  no_notation
    1.22    bot ("\<bottom>") and