removed junk (cf. 409d7f7247f4);
authorwenzelm
Mon, 14 Oct 2013 15:46:35 +0200
changeset 54338 7518a89965fe
parent 54337 2cf5d0a560ec
child 54339 26c790a6ce43
removed junk (cf. 409d7f7247f4);
src/Doc/IsarRef/HOL_Specific.thy
--- a/src/Doc/IsarRef/HOL_Specific.thy	Mon Oct 14 15:13:11 2013 +0200
+++ b/src/Doc/IsarRef/HOL_Specific.thy	Mon Oct 14 15:46:35 2013 +0200
@@ -2529,7 +2529,7 @@
     ;
 
     @@{command (HOL) code_include} target ( @{syntax string} ( @{syntax string} | '-') )
-    ;cite
+    ;
 
     @@{command (HOL) code_identifier} ( ( symbol_const | symbol_typeconstructor
       | symbol_class | symbol_class_relation | symbol_class_instance