# HG changeset patch
# User clasohm
# Date 826118379 -3600
# Node ID fe30812f5b5e3cda4191acc48d07762925f22de2
# Parent  2fd82cec17d403f73e5e2f0884721d74ca890428
added constdefs section

diff -r 2fd82cec17d4 -r fe30812f5b5e src/HOL/MiniML/Maybe.thy
--- a/src/HOL/MiniML/Maybe.thy	Wed Mar 06 14:12:24 1996 +0100
+++ b/src/HOL/MiniML/Maybe.thy	Wed Mar 06 14:19:39 1996 +0100
@@ -10,10 +10,9 @@
 
 datatype 'a maybe =  Ok 'a | Fail
 
-consts bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60)
-
-defs
-  bind_def "m bind f == case m of Ok r => f r | Fail => Fail"
+constdefs
+  bind :: ['a maybe, 'a => 'b maybe] => 'b maybe (infixl 60)
+  "m bind f == case m of Ok r => f r | Fail => Fail"
 
 syntax "@bind" :: [pttrns,'a maybe,'b] => 'c ("(_ := _;//_)" 0)
 translations "P := E; F" == "E bind (%P.F)"
diff -r 2fd82cec17d4 -r fe30812f5b5e src/HOL/MiniML/Type.thy
--- a/src/HOL/MiniML/Type.thy	Wed Mar 06 14:12:24 1996 +0100
+++ b/src/HOL/MiniML/Type.thy	Wed Mar 06 14:19:39 1996 +0100
@@ -28,10 +28,9 @@
 (* substitutions *)
 
 (* identity *)
-consts
+constdefs
         id_subst :: subst
-defs
-        id_subst_def "id_subst == (%n.TVar n)"
+        "id_subst == (%n.TVar n)"
 
 (* extension of substitution to type structures *)
 consts
@@ -54,16 +53,14 @@
         free_tv_Cons    "free_tv (x#l) = (free_tv x) Un (free_tv l)"
 
 (* domain of a substitution *)
-consts
+constdefs
         dom :: subst => nat set
-defs
-        dom_def         "dom s == {n. s n ~= TVar n}" 
+        "dom s == {n. s n ~= TVar n}" 
 
 (* codomain of a substitutions: the introduced variables *)
-consts
+constdefs
      cod :: subst => nat set
-defs
-        cod_def         "cod s == (UN m:dom s. free_tv (s m))"
+     "cod s == (UN m:dom s. free_tv (s m))"
 
 defs
         free_tv_subst   "free_tv s == (dom s) Un (cod s)"
@@ -71,10 +68,9 @@
 (* new_tv s n computes whether n is a new type variable w.r.t. a type 
    structure s, i.e. whether n is greater than any type variable 
    occuring in the type structure *)
-consts
+constdefs
         new_tv :: [nat,'a::type_struct] => bool
-defs
-        new_tv_def      "new_tv n ts == ! m. m:free_tv ts --> m<n"
+        "new_tv n ts == ! m. m:free_tv ts --> m<n"
 
 (* unification algorithm mgu *)
 consts