--- a/src/HOL/MiniML/Type.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/MiniML/Type.thy Fri Dec 01 12:03:13 1995 +0100
@@ -29,13 +29,13 @@
(* identity *)
consts
- id_subst :: "subst"
+ id_subst :: subst
defs
id_subst_def "id_subst == (%n.TVar n)"
(* extension of substitution to type structures *)
consts
- app_subst :: "[subst, 'a::type_struct] => 'a::type_struct" ("$")
+ app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
rules
app_subst_TVar "$ s (TVar n) = s n"
@@ -45,7 +45,7 @@
(* free_tv s: the type variables occuring freely in the type structure s *)
consts
- free_tv :: "['a::type_struct] => nat set"
+ free_tv :: ['a::type_struct] => nat set
rules
free_tv_TVar "free_tv (TVar m) = {m}"
@@ -55,13 +55,13 @@
(* domain of a substitution *)
consts
- dom :: "subst => nat set"
+ dom :: subst => nat set
defs
dom_def "dom s == {n. s n ~= TVar n}"
(* codomain of a substitutions: the introduced variables *)
consts
- cod :: "subst => nat set"
+ cod :: subst => nat set
defs
cod_def "cod s == (UN m:dom s. free_tv (s m))"
@@ -72,13 +72,13 @@
structure s, i.e. whether n is greater than any type variable
occuring in the type structure *)
consts
- new_tv :: "[nat,'a::type_struct] => bool"
+ new_tv :: [nat,'a::type_struct] => bool
defs
new_tv_def "new_tv n ts == ! m. m:free_tv ts --> m<n"
(* unification algorithm mgu *)
consts
- mgu :: "[type_expr,type_expr] => subst maybe"
+ mgu :: [type_expr,type_expr] => subst maybe
rules
mgu_eq "mgu t1 t2 = Ok u ==> $ u t1 = $ u t2"
mgu_mg "[| (mgu t1 t2) = Ok u; $ s t1 = $ s t2 |] ==>