src/HOL/Fun.thy
changeset 9141 49f6e45e7199
parent 8960 0cd01ec1830b
child 9309 4078d5e8b293
equal deleted inserted replaced
9140:69e8938c2409 9141:49f6e45e7199
     8 
     8 
     9 Fun = Vimage + equalities + 
     9 Fun = Vimage + equalities + 
    10 
    10 
    11 instance set :: (term) order
    11 instance set :: (term) order
    12                        (subset_refl,subset_trans,subset_antisym,psubset_eq)
    12                        (subset_refl,subset_trans,subset_antisym,psubset_eq)
    13 nonterminals
       
    14   updbinds  updbind
       
    15 
       
    16 consts
    13 consts
    17   fun_upd  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
    14   fun_upd  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
    18 
    15 
       
    16 nonterminals
       
    17   updbinds updbind
    19 syntax
    18 syntax
    20 
       
    21   (* Let expressions *)
       
    22 
       
    23   "_updbind"       :: ['a, 'a] => updbind             ("(2_ :=/ _)")
    19   "_updbind"       :: ['a, 'a] => updbind             ("(2_ :=/ _)")
    24   ""               :: updbind => updbinds             ("_")
    20   ""               :: updbind => updbinds             ("_")
    25   "_updbinds"      :: [updbind, updbinds] => updbinds ("_,/ _")
    21   "_updbinds"      :: [updbind, updbinds] => updbinds ("_,/ _")
    26   "_Update"        :: ['a, updbinds] => 'a            ("_/'((_)')" [1000,0] 900)
    22   "_Update"        :: ['a, updbinds] => 'a            ("_/'((_)')" [1000,0] 900)
    27 
    23