src/HOL/Tools/res_clause.ML
changeset 20790 a9595fdc02b1
parent 20422 35a6a4c863f1
child 20824 aca7d38283bf
     1.1 --- a/src/HOL/Tools/res_clause.ML	Sat Sep 30 14:31:02 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Sat Sep 30 14:31:41 2006 +0200
     1.3 @@ -118,7 +118,16 @@
     1.4  		   ("op :", "in"),
     1.5  		   ("op Un", "union"),
     1.6  		   ("op Int", "inter"),
     1.7 -		   ("List.op @", "append")];
     1.8 +		   ("List.op @", "append"),
     1.9 +		   ("Reconstruction.fequal", "fequal"),
    1.10 +		   ("Reconstruction.COMBI", "COMBI"),
    1.11 +		   ("Reconstruction.COMBK", "COMBK"),
    1.12 +		   ("Reconstruction.COMBB", "COMBB"),
    1.13 +		   ("Reconstruction.COMBC", "COMBC"),
    1.14 +		   ("Reconstruction.COMBS", "COMBS"),
    1.15 +		   ("Reconstruction.COMBB'", "COMBB_e"),
    1.16 +		   ("Reconstruction.COMBC'", "COMBC_e"),
    1.17 +		   ("Reconstruction.COMBS'", "COMBS_e")];
    1.18  
    1.19  val type_const_trans_table =
    1.20        Symtab.make [("*", "prod"),