src/Pure/Isar/isar_cmd.ML
changeset 7931 fa6fec415492
parent 7908 0b191b36ad97
child 7936 cbeaff0ef856
equal deleted inserted replaced
7930:220892918bd1 7931:fa6fec415492
    13   val quit: Toplevel.transition -> Toplevel.transition
    13   val quit: Toplevel.transition -> Toplevel.transition
    14   val touch_child_thys: string -> Toplevel.transition -> Toplevel.transition
    14   val touch_child_thys: string -> Toplevel.transition -> Toplevel.transition
    15   val touch_all_thys: Toplevel.transition -> Toplevel.transition
    15   val touch_all_thys: Toplevel.transition -> Toplevel.transition
    16   val touch_thy: string -> Toplevel.transition -> Toplevel.transition
    16   val touch_thy: string -> Toplevel.transition -> Toplevel.transition
    17   val remove_thy: string -> Toplevel.transition -> Toplevel.transition
    17   val remove_thy: string -> Toplevel.transition -> Toplevel.transition
       
    18   val kill_thy: string -> Toplevel.transition -> Toplevel.transition
    18   val cannot_undo: string -> Toplevel.transition -> Toplevel.transition
    19   val cannot_undo: string -> Toplevel.transition -> Toplevel.transition
    19   val clear_undos_theory: int -> Toplevel.transition -> Toplevel.transition
    20   val clear_undos_theory: int -> Toplevel.transition -> Toplevel.transition
    20   val redo: Toplevel.transition -> Toplevel.transition
    21   val redo: Toplevel.transition -> Toplevel.transition
    21   val undos_proof: int -> Toplevel.transition -> Toplevel.transition
    22   val undos_proof: int -> Toplevel.transition -> Toplevel.transition
    22   val kill_proof: Toplevel.transition -> Toplevel.transition
    23   val kill_proof: Toplevel.transition -> Toplevel.transition
    69 
    70 
    70 fun touch_child_thys name = Toplevel.imperative (fn () => ThyInfo.touch_child_thys name);
    71 fun touch_child_thys name = Toplevel.imperative (fn () => ThyInfo.touch_child_thys name);
    71 val touch_all_thys = Toplevel.imperative ThyInfo.touch_all_thys;
    72 val touch_all_thys = Toplevel.imperative ThyInfo.touch_all_thys;
    72 fun touch_thy name = Toplevel.imperative (fn () => ThyInfo.touch_thy name);
    73 fun touch_thy name = Toplevel.imperative (fn () => ThyInfo.touch_thy name);
    73 fun remove_thy name = Toplevel.imperative (fn () => ThyInfo.remove_thy name);
    74 fun remove_thy name = Toplevel.imperative (fn () => ThyInfo.remove_thy name);
       
    75 fun kill_thy name = Toplevel.imperative (fn () => IsarThy.kill_theory name);
    74 
    76 
    75 
    77 
    76 (* history commands *)
    78 (* history commands *)
    77 
    79 
    78 fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt));
    80 fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt));