buid Pur, HOL worked decompose-isar
authorWalther Neuper <neuper@ist.tugraz.at>
Fri, 25 Feb 2011 13:26:45 +0100
branchdecompose-isar
changeset 41898964d4a77a03f
parent 41897 355be7f60389
child 41899 d837e83a4835
buid Pur, HOL worked
etc/components
src/Pure/thm.ML
src/Tools/isac/Build_Isac.thy
     1.1 --- a/etc/components	Fri Feb 25 13:04:56 2011 +0100
     1.2 +++ b/etc/components	Fri Feb 25 13:26:45 2011 +0100
     1.3 @@ -7,7 +7,6 @@
     1.4  src/CTT
     1.5  src/Cube
     1.6  src/FOLP
     1.7 -src/HOLCF
     1.8  src/LCF
     1.9  src/Sequents
    1.10  #misc components
    1.11 @@ -19,10 +18,3 @@
    1.12  src/HOL/Tools/SMT
    1.13  src/HOL/Tools/Predicate_Compile
    1.14  src/HOL/Mutabelle
    1.15 -
    1.16 -#bundled components
    1.17 -contrib/e-1.0-004
    1.18 -contrib/jedit-4.3.2
    1.19 -contrib/kodkodi-1.2.13
    1.20 -contrib/scala-2.8.0.RC5
    1.21 -contrib/spass-3.7
     2.1 --- a/src/Pure/thm.ML	Fri Feb 25 13:04:56 2011 +0100
     2.2 +++ b/src/Pure/thm.ML	Fri Feb 25 13:26:45 2011 +0100
     2.3 @@ -53,8 +53,8 @@
     2.4     {thy_ref: theory_ref,       (*new since 2002*)
     2.5      tags: Properties.T,        (*new since 2002*)
     2.6      maxidx: int,
     2.7 -    shyps: sort OrdList.T,
     2.8 -    hyps: term OrdList.T,
     2.9 +    shyps: sort Ord_List.T,
    2.10 +    hyps: term Ord_List.T,
    2.11      tpairs: (term * term) list,(*new since 2002*)
    2.12      prop: term}
    2.13    val crep_thm: thm ->
    2.14 @@ -78,8 +78,8 @@
    2.15  		       theory_ref -> 
    2.16  		       Properties.T -> 
    2.17  		       int -> 
    2.18 -		       sort OrdList.T -> 
    2.19 -		       term OrdList.T ->
    2.20 +		       sort Ord_List.T -> 
    2.21 +		       term Ord_List.T ->
    2.22  		       (term * term) list ->
    2.23  		       term ->
    2.24  		       thm
     3.1 --- a/src/Tools/isac/Build_Isac.thy	Fri Feb 25 13:04:56 2011 +0100
     3.2 +++ b/src/Tools/isac/Build_Isac.thy	Fri Feb 25 13:26:45 2011 +0100
     3.3 @@ -20,7 +20,8 @@
     3.4  header {* Loading the isac mathengine *}
     3.5  
     3.6  theory Build_Isac
     3.7 -imports Complex_Main "ProgLang/Language" (*"Knowledge/Isac"*)
     3.8 +(*imports Complex_Main "ProgLang/Language" (*"Knowledge/Isac"*)*)
     3.9 +imports Complex_Main
    3.10  begin
    3.11  
    3.12  ML {*