added Induct/Common_Patterns.thy;
authorwenzelm
Sun Sep 16 21:04:44 2007 +0200 (2007-09-16)
changeset 24607fc06b84acd81
parent 24606 7acbb982fc77
child 24608 aae1095dbe3b
added Induct/Common_Patterns.thy;
src/HOL/Induct/ROOT.ML
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/Induct/ROOT.ML	Sun Sep 16 21:04:43 2007 +0200
     1.2 +++ b/src/HOL/Induct/ROOT.ML	Sun Sep 16 21:04:44 2007 +0200
     1.3 @@ -1,6 +1,9 @@
     1.4  
     1.5  (* $Id$ *)
     1.6  
     1.7 +setmp quick_and_dirty true
     1.8 +  use_thy "Common_Patterns";
     1.9 +
    1.10  use_thys ["Mutil", "QuoDataType", "QuoNestedDataType", "Term",
    1.11    "ABexp", "Tree", "Ordinals", "Sigma_Algebra", "Comb", "PropLog",
    1.12    "SList", "LFilter", "Com"];
     2.1 --- a/src/HOL/IsaMakefile	Sun Sep 16 21:04:43 2007 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Sun Sep 16 21:04:44 2007 +0200
     2.3 @@ -248,7 +248,7 @@
     2.4  HOL-Induct: HOL $(LOG)/HOL-Induct.gz
     2.5  
     2.6  $(LOG)/HOL-Induct.gz: $(OUT)/HOL \
     2.7 -  Induct/Com.thy Induct/Comb.thy Induct/LFilter.thy \
     2.8 +  Induct/Common_Patterns.thy Induct/Com.thy Induct/Comb.thy Induct/LFilter.thy \
     2.9    Induct/LList.thy Induct/Mutil.thy Induct/Ordinals.thy \
    2.10    Induct/PropLog.thy Induct/QuoNestedDataType.thy Induct/QuoDataType.thy\
    2.11    Induct/ROOT.ML \