src/Pure/Isar/isar_syn.ML
changeset 6196 f9fdb4e29790
parent 6108 2c9ed58c30ba
child 6197 4328d436c556
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Feb 03 16:49:04 1999 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Feb 03 16:49:36 1999 +0100
     1.3 @@ -464,12 +464,12 @@
     1.4      (Scan.succeed IsarCmd.pwd);
     1.5  
     1.6  val use_thyP =
     1.7 -  OuterSyntax.parser true "use_thy" "use_thy theory file"
     1.8 +  OuterSyntax.parser true "use_thy" "use theory file"
     1.9      (name >> IsarCmd.use_thy);
    1.10  
    1.11 -val loadP =
    1.12 -  OuterSyntax.parser true "load" "load theory file"
    1.13 -    (name >> IsarCmd.load);
    1.14 +val update_thyP =
    1.15 +  OuterSyntax.parser true "update_thy" "update theory file"
    1.16 +    (name >> IsarCmd.use_thy);
    1.17  
    1.18  val prP =
    1.19    OuterSyntax.parser true "pr" "print current toplevel state"
    1.20 @@ -532,13 +532,13 @@
    1.21    print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,
    1.22    print_thmsP, print_propP, print_termP, print_typeP,
    1.23    (*system commands*)
    1.24 -  cdP, pwdP, use_thyP, loadP, prP, commitP, quitP, exitP, restartP, breakP];
    1.25 +  cdP, pwdP, use_thyP, update_thyP, prP, commitP, quitP, exitP,
    1.26 +  restartP, breakP];
    1.27  
    1.28  
    1.29  end;
    1.30  
    1.31  
    1.32 -(* install the Pure outer syntax *)
    1.33 -
    1.34 +(*install the Pure outer syntax*)
    1.35  OuterSyntax.add_keywords IsarSyn.keywords;
    1.36  OuterSyntax.add_parsers IsarSyn.parsers;