added axclass "one" and polymorphic const "1";
authorwenzelm
Fri Oct 05 21:49:15 2001 +0200 (2001-10-05)
changeset 116983b3feb92207a
parent 11697 8dd899efbd35
child 11699 c7df55158574
added axclass "one" and polymorphic const "1";
print consts "0" and "1" with type constraints;
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Fri Oct 05 21:48:04 2001 +0200
     1.2 +++ b/src/HOL/HOL.thy	Fri Oct 05 21:49:15 2001 +0200
     1.3 @@ -54,8 +54,9 @@
     1.4  
     1.5  (* Overloaded Constants *)
     1.6  
     1.7 -axclass zero  < "term"
     1.8 -axclass plus  < "term"
     1.9 +axclass zero < "term"
    1.10 +axclass one < "term"
    1.11 +axclass plus < "term"
    1.12  axclass minus < "term"
    1.13  axclass times < "term"
    1.14  axclass inverse < "term"
    1.15 @@ -64,11 +65,20 @@
    1.16  
    1.17  consts
    1.18    "0"           :: "'a::zero"                       ("0")
    1.19 +  "1"           :: "'a::one"                        ("1")
    1.20    "+"           :: "['a::plus, 'a]  => 'a"          (infixl 65)
    1.21    -             :: "['a::minus, 'a] => 'a"          (infixl 65)
    1.22    uminus        :: "['a::minus] => 'a"              ("- _" [81] 80)
    1.23    *             :: "['a::times, 'a] => 'a"          (infixl 70)
    1.24  
    1.25 +typed_print_translation {*
    1.26 +  let
    1.27 +    fun tr' c = (c, fn show_sorts => fn T => fn ts =>
    1.28 +      if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match
    1.29 +      else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
    1.30 +  in [tr' "0", tr' "1"] end;
    1.31 +*}
    1.32 +
    1.33  local
    1.34  
    1.35  consts