added "_update_name" and parse_translation;
authorwenzelm
Mon Dec 11 20:10:18 2000 +0100 (2000-12-11)
changeset 10641d1533f63c738
parent 10640 562e20e543b1
child 10642 5be46cd1f94a
added "_update_name" and parse_translation;
src/HOL/Record.thy
     1.1 --- a/src/HOL/Record.thy	Mon Dec 11 20:09:47 2000 +0100
     1.2 +++ b/src/HOL/Record.thy	Mon Dec 11 20:10:18 2000 +0100
     1.3 @@ -35,6 +35,7 @@
     1.4    "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
     1.5  
     1.6    (*record updates*)
     1.7 +  "_update_name"        :: idt
     1.8    "_update"             :: "[ident, 'a] => update"                      ("(2_ :=/ _)")
     1.9    ""                    :: "update => updates"                          ("_")
    1.10    "_updates"            :: "[update, updates] => updates"               ("_,/ _")
    1.11 @@ -47,6 +48,19 @@
    1.12    "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
    1.13    "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
    1.14  
    1.15 +parse_translation {*
    1.16 +  let
    1.17 +    fun update_name_tr (Free (x, T) :: ts) =
    1.18 +          Term.list_comb (Free (suffix RecordPackage.updateN x, T), ts)
    1.19 +      | update_name_tr (Const (x, T) :: ts) =
    1.20 +          Term.list_comb (Const (suffix RecordPackage.updateN x, T), ts)
    1.21 +      | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
    1.22 +          Term.list_comb (c $ update_name_tr [t] $
    1.23 +            (Syntax.const "fun" $ ty $ Syntax.const "dummy"), ts)
    1.24 +      | update_name_tr ts = raise TERM ("update_name_tr", ts);
    1.25 +  in [("_update_name", update_name_tr)] end
    1.26 +*}
    1.27 +
    1.28  
    1.29  (* type class for record extensions *)
    1.30