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.
'classrel' now allows multiple arguments;
authorwenzelm
Fri, 21 May 2004 21:20:38 +0200
changeset 14779 e15d4bd7fe71
parent 14778 69cafc301399
child 14780 949a3f558a43
'classrel' now allows multiple arguments;
src/Pure/Isar/isar_syn.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/isar_syn.ML	Fri May 21 21:20:14 2004 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri May 21 21:20:38 2004 +0200
@@ -89,8 +89,8 @@
 
 val classrelP =
   OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl
-    (P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
-    >> (Toplevel.theory o Theory.add_classrel o single));
+    (P.and_list1 (P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname))
+    >> (Toplevel.theory o Theory.add_classrel));
 
 val defaultsortP =
   OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl
isabelle