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 hol_rewrite_cterm (use full_rewrite_cterm from Pure);
authorwenzelm
Thu, 04 Oct 2001 15:40:31 +0200
changeset 11684 abd396ca7ef9
parent 11683 f2268239b93f
child 11685 c786d9ce558e
removed hol_rewrite_cterm (use full_rewrite_cterm from Pure);
src/HOL/simpdata.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/simpdata.ML	Thu Oct 04 15:40:05 2001 +0200
+++ b/src/HOL/simpdata.ML	Thu Oct 04 15:40:31 2001 +0200
@@ -390,8 +390,6 @@
      addsplits [split_if];
 
 fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews);
-fun hol_rewrite_cterm rews =
-  #2 o Thm.dest_comb o #prop o Thm.crep_thm o Simplifier.full_rewrite (HOL_basic_ss addsimps rews);
 
 
 (*Simplifies x assuming c and y assuming ~c*)
isabelle