added constdefs section
authorclasohm
Wed Mar 06 14:19:39 1996 +0100 (1996-03-06)
changeset 1557fe30812f5b5e
parent 1556 2fd82cec17d4
child 1558 9c6ebfab4e05
added constdefs section
src/HOL/MiniML/Maybe.thy
src/HOL/MiniML/Type.thy
     1.1 --- a/src/HOL/MiniML/Maybe.thy	Wed Mar 06 14:12:24 1996 +0100
     1.2 +++ b/src/HOL/MiniML/Maybe.thy	Wed Mar 06 14:19:39 1996 +0100
     1.3 @@ -10,10 +10,9 @@
     1.4  
     1.5  datatype 'a maybe =  Ok 'a | Fail
     1.6  
     1.7 -consts bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60)
     1.8 -
     1.9 -defs
    1.10 -  bind_def "m bind f == case m of Ok r => f r | Fail => Fail"
    1.11 +constdefs
    1.12 +  bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60)
    1.13 +  "m bind f == case m of Ok r => f r | Fail => Fail"
    1.14  
    1.15  syntax "@bind" :: [pttrns,'a maybe,'b] => 'c ("(_ := _;//_)" 0)
    1.16  translations "P := E; F" == "E bind (%P.F)"
     2.1 --- a/src/HOL/MiniML/Type.thy	Wed Mar 06 14:12:24 1996 +0100
     2.2 +++ b/src/HOL/MiniML/Type.thy	Wed Mar 06 14:19:39 1996 +0100
     2.3 @@ -28,10 +28,9 @@
     2.4  (* substitutions *)
     2.5  
     2.6  (* identity *)
     2.7 -consts
     2.8 +constdefs
     2.9          id_subst :: subst
    2.10 -defs
    2.11 -        id_subst_def "id_subst == (%n.TVar n)"
    2.12 +        "id_subst == (%n.TVar n)"
    2.13  
    2.14  (* extension of substitution to type structures *)
    2.15  consts
    2.16 @@ -54,16 +53,14 @@
    2.17          free_tv_Cons    "free_tv (x#l) = (free_tv x) Un (free_tv l)"
    2.18  
    2.19  (* domain of a substitution *)
    2.20 -consts
    2.21 +constdefs
    2.22          dom :: subst => nat set
    2.23 -defs
    2.24 -        dom_def         "dom s == {n. s n ~= TVar n}" 
    2.25 +        "dom s == {n. s n ~= TVar n}" 
    2.26  
    2.27  (* codomain of a substitutions: the introduced variables *)
    2.28 -consts
    2.29 +constdefs
    2.30       cod :: subst => nat set
    2.31 -defs
    2.32 -        cod_def         "cod s == (UN m:dom s. free_tv (s m))"
    2.33 +     "cod s == (UN m:dom s. free_tv (s m))"
    2.34  
    2.35  defs
    2.36          free_tv_subst   "free_tv s == (dom s) Un (cod s)"
    2.37 @@ -71,10 +68,9 @@
    2.38  (* new_tv s n computes whether n is a new type variable w.r.t. a type 
    2.39     structure s, i.e. whether n is greater than any type variable 
    2.40     occuring in the type structure *)
    2.41 -consts
    2.42 +constdefs
    2.43          new_tv :: [nat,'a::type_struct] => bool
    2.44 -defs
    2.45 -        new_tv_def      "new_tv n ts == ! m. m:free_tv ts --> m<n"
    2.46 +        "new_tv n ts == ! m. m:free_tv ts --> m<n"
    2.47  
    2.48  (* unification algorithm mgu *)
    2.49  consts