src/HOL/Auth/DB-ROOT.ML
changeset 2563 e908e2716f3a
parent 2326 6df4488339e4
child 3511 da4dd8b7ced4
equal deleted inserted replaced
2562:d571d6660240 2563:e908e2716f3a
    12 val banner = "Security Protocols";
    12 val banner = "Security Protocols";
    13 writeln banner;
    13 writeln banner;
    14 
    14 
    15 init_thy_reader();
    15 init_thy_reader();
    16 
    16 
    17 (*Must be redefined in order to refer to the new instance of bind_thm
       
    18   created by init_thy_reader.*)
       
    19 fun qed_spec_mp name =
       
    20   let val thm = normalize_thm [RSspec,RSmp] (result())
       
    21   in bind_thm(name, thm) end;
       
    22 
       
    23 use_thy "Message";
    17 use_thy "Message";
    24 
    18