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.
delsimprocs [unit_eq_proc];
authorwenzelm
Thu, 25 Jun 1998 16:13:20 +0200
changeset 5086 ef479934678b
parent 5085 8e5a7942fdea
child 5087 ee8a754f1981
delsimprocs [unit_eq_proc];
src/HOL/Induct/LList.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Induct/LList.ML	Thu Jun 25 16:12:02 1998 +0200
+++ b/src/HOL/Induct/LList.ML	Thu Jun 25 16:13:20 1998 +0200
@@ -10,7 +10,7 @@
 
 (** Simplification **)
 
-simpset_ref() := simpset() addsplits [split_split, split_sum_case];
+simpset_ref() := simpset() addsplits [split_split, split_sum_case] delsimprocs [unit_eq_proc];
 
 
 (*This justifies using llist in other recursive type definitions*)
isabelle