src/Pure/Isar/isar_cmd.ML
changeset 6694 335833a8b10a
parent 6686 08b06cd19f8d
child 6734 151c07f5b70a
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri May 21 16:23:18 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri May 21 16:23:48 1999 +0200
     1.3 @@ -22,6 +22,7 @@
     1.4    val cd: string -> Toplevel.transition -> Toplevel.transition
     1.5    val pwd: Toplevel.transition -> Toplevel.transition
     1.6    val use_thy: string -> Toplevel.transition -> Toplevel.transition
     1.7 +  val use_thy_only: string -> Toplevel.transition -> Toplevel.transition
     1.8    val update_thy: string -> Toplevel.transition -> Toplevel.transition
     1.9    val print_theory: Toplevel.transition -> Toplevel.transition
    1.10    val print_syntax: Toplevel.transition -> Toplevel.transition
    1.11 @@ -97,6 +98,7 @@
    1.12  (* load theory files *)
    1.13  
    1.14  fun use_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy name);
    1.15 +fun use_thy_only name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy_only name);
    1.16  fun update_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.update_thy name);
    1.17  
    1.18