# HG changeset patch
# User wenzelm
# Date 1002311355 -7200
# Node ID 3b3feb92207a9e6d9cd13deac035422720219d05
# Parent  8dd899efbd35bb2149aaeccbccf8e127eecac285
added axclass "one" and polymorphic const "1";
print consts "0" and "1" with type constraints;

diff -r 8dd899efbd35 -r 3b3feb92207a src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Oct 05 21:48:04 2001 +0200
+++ b/src/HOL/HOL.thy	Fri Oct 05 21:49:15 2001 +0200
@@ -54,8 +54,9 @@
 
 (* Overloaded Constants *)
 
-axclass zero  < "term"
-axclass plus  < "term"
+axclass zero < "term"
+axclass one < "term"
+axclass plus < "term"
 axclass minus < "term"
 axclass times < "term"
 axclass inverse < "term"
@@ -64,11 +65,20 @@
 
 consts
   "0"           :: "'a::zero"                       ("0")
+  "1"           :: "'a::one"                        ("1")
   "+"           :: "['a::plus, 'a]  => 'a"          (infixl 65)
   -             :: "['a::minus, 'a] => 'a"          (infixl 65)
   uminus        :: "['a::minus] => 'a"              ("- _" [81] 80)
   *             :: "['a::times, 'a] => 'a"          (infixl 70)
 
+typed_print_translation {*
+  let
+    fun tr' c = (c, fn show_sorts => fn T => fn ts =>
+      if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match
+      else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
+  in [tr' "0", tr' "1"] end;
+*}
+
 local
 
 consts