Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Remove trailing whitespace in src/num/termination/TotalDefn.sml

  • Loading branch information...
commit 9ee0a824a4e0f7480ce17fd33e162ab16d4c2ef9 1 parent 30fca47
@mn200 mn200 authored
Showing with 4 additions and 4 deletions.
  1. +4 −4 src/num/termination/TotalDefn.sml
View
8 src/num/termination/TotalDefn.sml
@@ -113,18 +113,18 @@ fun mk_lex_reln argvars sizedlist arrangement =
(* x.fld is a proper subterm of x. *)
(*---------------------------------------------------------------------------*)
-fun is_recd_proj tm1 tm2 =
+fun is_recd_proj tm1 tm2 =
let val (proj,a) = dest_comb tm1
val aty = type_of a
- val projlist = mapfilter
+ val projlist = mapfilter
(fst o dest_comb o boolSyntax.lhs o snd o strip_forall o concl)
(TypeBase.accessors_of aty)
in TypeBase.is_record_type aty andalso mem proj projlist
end
handle HOL_ERR _ => false;
-
+
fun proper_subterm tm1 tm2 =
- not(aconv tm1 tm2)
+ not(aconv tm1 tm2)
andalso (Lib.can (find_term (aconv tm1)) tm2
orelse
is_recd_proj tm1 tm2);
Please sign in to comment.
Something went wrong with that request. Please try again.