| author | nipkow | 
| Tue, 07 Sep 2010 10:05:19 +0200 | |
| changeset 39198 | f967a16dfcdd | 
| parent 38767 | d8da44a8dd25 | 
| child 42651 | e3fdb7c96be5 | 
| permissions | -rw-r--r-- | 
quick_and_dirty := true; Thy_Output.source_default := true; use "../../antiquote_setup.ML"; use_thys [ "Introduction", "Framework", "First_Order_Logic", "Outer_Syntax", "Document_Preparation", "Spec", "Proof", "Inner_Syntax", "Misc", "Generic", "HOL_Specific", "Quick_Reference", "Symbols", "ML_Tactic" ];