tuned;
authorwenzelm
Sun Jun 25 23:58:27 2000 +0200 (2000-06-25)
changeset 914149f6e45e7199
parent 9140 69e8938c2409
child 9142 d5a841f89e92
tuned;
src/HOL/Fun.thy
     1.1 --- a/src/HOL/Fun.thy	Sun Jun 25 23:57:29 2000 +0200
     1.2 +++ b/src/HOL/Fun.thy	Sun Jun 25 23:58:27 2000 +0200
     1.3 @@ -10,16 +10,12 @@
     1.4  
     1.5  instance set :: (term) order
     1.6                         (subset_refl,subset_trans,subset_antisym,psubset_eq)
     1.7 -nonterminals
     1.8 -  updbinds  updbind
     1.9 -
    1.10  consts
    1.11    fun_upd  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
    1.12  
    1.13 +nonterminals
    1.14 +  updbinds updbind
    1.15  syntax
    1.16 -
    1.17 -  (* Let expressions *)
    1.18 -
    1.19    "_updbind"       :: ['a, 'a] => updbind             ("(2_ :=/ _)")
    1.20    ""               :: updbind => updbinds             ("_")
    1.21    "_updbinds"      :: [updbind, updbinds] => updbinds ("_,/ _")