Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned layout;
authorwenzelm
Wed, 30 Nov 2011 16:05:15 +0100
changeset 45693 bbd2c7ffc02c
parent 45692 d2567e55af83
child 45694 4a8743618257
tuned layout;
src/HOL/Typerep.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Typerep.thy	Wed Nov 30 16:03:18 2011 +0100
+++ b/src/HOL/Typerep.thy	Wed Nov 30 16:05:15 2011 +0100
@@ -63,8 +63,9 @@
     |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
   end;
 
-fun ensure_typerep tyco thy = if not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep})
-  andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort type}
+fun ensure_typerep tyco thy =
+  if not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep})
+    andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort type}
   then add_typerep tyco thy else thy;
 
 in
isabelle