replaced "rules" by "primrec"
authornipkow
Mon, 25 Mar 1996 08:46:02 +0100
changeset 1604 cff41d1094ad
parent 1603 44bc1417b07c
child 1605 248e1e125ca0
replaced "rules" by "primrec"
src/HOL/MiniML/Type.thy
--- a/src/HOL/MiniML/Type.thy	Sun Mar 24 18:36:28 1996 +0100
+++ b/src/HOL/MiniML/Type.thy	Mon Mar 25 08:46:02 1996 +0100
@@ -36,9 +36,10 @@
 consts
         app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
 
-rules
-        app_subst_TVar  "$ s (TVar n) = s n" 
-        app_subst_Fun   "$ s (t1 -> t2) = ($ s t1) -> ($ s t2)" 
+primrec app_subst typ
+  app_subst_TVar  "$ s (TVar n) = s n" 
+  app_subst_Fun   "$ s (t1 -> t2) = ($ s t1) -> ($ s t2)" 
+
 defs
         app_subst_list  "$ s == map ($ s)"