author | wenzelm |

Thu Feb 12 16:54:01 1998 +0100 (1998-02-12) | |

changeset 4626 | 51dd12f34c78 |

parent 4625 | 9c6082518cfb |

child 4627 | ae95666c71cc |

tuned comments;

1.1 --- a/src/Pure/term.ML Thu Feb 12 16:43:05 1998 +0100 1.2 +++ b/src/Pure/term.ML Thu Feb 12 16:54:01 1998 +0100 1.3 @@ -176,7 +176,7 @@ 1.4 for resolution.*) 1.5 type indexname = string*int; 1.6 1.7 -(* Types are classified by classes. *) 1.8 +(* Types are classified by sorts. *) 1.9 type class = string; 1.10 type sort = class list; 1.11 1.12 @@ -193,7 +193,7 @@ 1.13 1.14 (*terms. Bound variables are indicated by depth number. 1.15 Free variables, (scheme) variables and constants have names. 1.16 - An term is "closed" if there every bound variable of level "lev" 1.17 + An term is "closed" if every bound variable of level "lev" 1.18 is enclosed by at least "lev" abstractions. 1.19 1.20 It is possible to create meaningless terms containing loose bound vars 1.21 @@ -446,7 +446,7 @@ 1.22 1.23 (*Substitute arguments for loose bound variables. 1.24 Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi). 1.25 - Note that for ((x,y)c)(a,b), the bound vars in c are x=1 and y=0 1.26 + Note that for ((%x y. c) a b), the bound vars in c are x=1 and y=0 1.27 and the appropriate call is subst_bounds([b,a], c) . 1.28 Loose bound variables >=n are reduced by "n" to 1.29 compensate for the disappearance of lambdas. 1.30 @@ -490,7 +490,7 @@ 1.31 fun ins_ix (x,xs) = if mem_ix (x, xs) then xs else x :: xs; 1.32 1.33 (*Tests whether 2 terms are alpha-convertible and have same type. 1.34 - Note that constants and Vars may have more than one type.*) 1.35 + Note that constants may have more than one type.*) 1.36 fun (Const(a,T)) aconv (Const(b,U)) = a=b andalso T=U 1.37 | (Free(a,T)) aconv (Free(b,U)) = a=b andalso T=U 1.38 | (Var(v,T)) aconv (Var(w,U)) = eq_ix(v,w) andalso T=U 1.39 @@ -670,7 +670,7 @@ 1.40 (**** Syntax-related declarations ****) 1.41 1.42 1.43 -(*Dummy type for parsing. Will be replaced during type inference. *) 1.44 +(*Dummy type for parsing and printing. Will be replaced during type inference. *) 1.45 val dummyT = Type("dummy",[]); 1.46 1.47 (*scan a numeral of the given radix, normally 10*)