src/Pure/Isar/isar_syn.ML
changeset 7908 0b191b36ad97
parent 7891 c77ad0c3c92f
child 7931 fa6fec415492
equal deleted inserted replaced
7907:258f136864db 7908:0b191b36ad97
   551     (P.name >> IsarCmd.touch_thy);
   551     (P.name >> IsarCmd.touch_thy);
   552 
   552 
   553 val touch_all_thysP =
   553 val touch_all_thysP =
   554   OuterSyntax.improper_command "touch_all_thys" "outdate all non-finished theories" K.diag
   554   OuterSyntax.improper_command "touch_all_thys" "outdate all non-finished theories" K.diag
   555     (Scan.succeed IsarCmd.touch_all_thys);
   555     (Scan.succeed IsarCmd.touch_all_thys);
       
   556 
       
   557 val touch_child_thysP =
       
   558   OuterSyntax.improper_command "touch_child_thys" "outdate child theories" K.diag
       
   559     (P.name >> IsarCmd.touch_child_thys);
   556 
   560 
   557 val remove_thyP =
   561 val remove_thyP =
   558   OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag
   562   OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag
   559     (P.name >> IsarCmd.remove_thy);
   563     (P.name >> IsarCmd.remove_thy);
   560 
   564 
   630   print_syntaxP, print_theoremsP, print_attributesP, print_methodsP,
   634   print_syntaxP, print_theoremsP, print_attributesP, print_methodsP,
   631   thms_containingP, print_bindsP, print_lthmsP, print_thmsP,
   635   thms_containingP, print_bindsP, print_lthmsP, print_thmsP,
   632   print_propP, print_termP, print_typeP,
   636   print_propP, print_termP, print_typeP,
   633   (*system commands*)
   637   (*system commands*)
   634   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
   638   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
   635   touch_thyP, touch_all_thysP, remove_thyP, prP, disable_prP,
   639   touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP, prP,
   636   enable_prP, commitP, quitP, exitP, init_toplevelP, welcomeP];
   640   disable_prP, enable_prP, commitP, quitP, exitP, init_toplevelP,
       
   641   welcomeP];
   637 
   642 
   638 
   643 
   639 end;
   644 end;
   640 
   645 
   641 
   646