# 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