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.
Removed unnecessary Addsimps.
authorberghofe
Thu, 08 Aug 1996 11:45:04 +0200
changeset 1901 0a4fbd097ce0
parent 1900 c7a869229091
child 1902 e349b91cf197
Removed unnecessary Addsimps.
src/HOL/MiniML/Type.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/MiniML/Type.ML	Thu Aug 08 11:34:29 1996 +0200
+++ b/src/HOL/MiniML/Type.ML	Thu Aug 08 11:45:04 1996 +0200
@@ -1,8 +1,6 @@
 open Type;
 
-Addsimps [app_subst_TVar,app_subst_Fun];
 Addsimps [mgu_eq,mgu_mg,mgu_free];
-Addsimps [free_tv_TVar,free_tv_Fun,free_tv_Nil,free_tv_Cons];
 
 (* mgu does not introduce new type variables *)
 goalw thy [new_tv_def]
isabelle