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.
minor adaption for SML/NJ
authoroheimb
Wed, 12 Aug 1998 17:40:18 +0200
changeset 5307 6a699d5cdef4
parent 5306 3d1368a3a2a2
child 5308 3ca4da83012c
minor adaption for SML/NJ
src/FOL/simpdata.ML file | annotate | diff | comparison | revisions
src/HOL/simpdata.ML file | annotate | diff | comparison | revisions 
--- a/src/FOL/simpdata.ML	Wed Aug 12 16:49:25 1998 +0200
+++ b/src/FOL/simpdata.ML	Wed Aug 12 17:40:18 1998 +0200
@@ -259,8 +259,8 @@
 val split_tac        = Splitter.split_tac;
 val split_inside_tac = Splitter.split_inside_tac;
 val split_asm_tac    = Splitter.split_asm_tac;
-val addsplits        = Splitter.addsplits;
-val delsplits        = Splitter.delsplits;
+val op addsplits     = Splitter.addsplits;
+val op delsplits     = Splitter.delsplits;
 val Addsplits        = Splitter.Addsplits;
 val Delsplits        = Splitter.Delsplits;
 
--- a/src/HOL/simpdata.ML	Wed Aug 12 16:49:25 1998 +0200
+++ b/src/HOL/simpdata.ML	Wed Aug 12 17:40:18 1998 +0200
@@ -344,8 +344,8 @@
 val split_tac        = Splitter.split_tac;
 val split_inside_tac = Splitter.split_inside_tac;
 val split_asm_tac    = Splitter.split_asm_tac;
-val addsplits        = Splitter.addsplits;
-val delsplits        = Splitter.delsplits;
+val op addsplits     = Splitter.addsplits;
+val op delsplits     = Splitter.delsplits;
 val Addsplits        = Splitter.Addsplits;
 val Delsplits        = Splitter.Delsplits;
isabelle