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.
Added the combinator constants to the constants table.
authormengj
Sat, 30 Sep 2006 14:31:41 +0200
changeset 20790 a9595fdc02b1
parent 20789 e279499c4f80
child 20791 497e1c9d4a9f
Added the combinator constants to the constants table.
src/HOL/Tools/res_clause.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/res_clause.ML	Sat Sep 30 14:31:02 2006 +0200
+++ b/src/HOL/Tools/res_clause.ML	Sat Sep 30 14:31:41 2006 +0200
@@ -118,7 +118,16 @@
 		   ("op :", "in"),
 		   ("op Un", "union"),
 		   ("op Int", "inter"),
-		   ("List.op @", "append")];
+		   ("List.op @", "append"),
+		   ("Reconstruction.fequal", "fequal"),
+		   ("Reconstruction.COMBI", "COMBI"),
+		   ("Reconstruction.COMBK", "COMBK"),
+		   ("Reconstruction.COMBB", "COMBB"),
+		   ("Reconstruction.COMBC", "COMBC"),
+		   ("Reconstruction.COMBS", "COMBS"),
+		   ("Reconstruction.COMBB'", "COMBB_e"),
+		   ("Reconstruction.COMBC'", "COMBC_e"),
+		   ("Reconstruction.COMBS'", "COMBS_e")];
 
 val type_const_trans_table =
       Symtab.make [("*", "prod"),
isabelle