src/HOL/HOL.thy
changeset 22993 838c66e760b5
parent 22839 ede26eb5e549
child 23037 6c72943a71b1
     1.1 --- a/src/HOL/HOL.thy	Thu May 17 19:29:39 2007 +0200
     1.2 +++ b/src/HOL/HOL.thy	Thu May 17 19:49:16 2007 +0200
     1.3 @@ -227,7 +227,7 @@
     1.4    fun tr' c = (c, fn show_sorts => fn T => fn ts =>
     1.5      if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match
     1.6      else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
     1.7 -in map tr' [@{const_syntax "HOL.one"}, @{const_syntax "HOL.zero"}] end;
     1.8 +in map tr' [@{const_syntax HOL.one}, @{const_syntax HOL.zero}] end;
     1.9  *} -- {* show types that are presumably too general *}
    1.10  
    1.11  
    1.12 @@ -913,7 +913,7 @@
    1.13  struct
    1.14    type claset = Classical.claset
    1.15    val equality_name = @{const_name "op ="}
    1.16 -  val not_name = @{const_name "Not"}
    1.17 +  val not_name = @{const_name Not}
    1.18    val notE = @{thm HOL.notE}
    1.19    val ccontr = @{thm HOL.ccontr}
    1.20    val contr_tac = Classical.contr_tac