# HG changeset patch # User urbanc # Date 1180063136 -7200 # Node ID 11e1a67fbfe8b71347d89876f25dc75b478ebedf # Parent f4779adcd1a2702b5e2c9ddcbb16e9328c2f1721 took out Class.thy from the compiling process until memory problems are solved diff -r f4779adcd1a2 -r 11e1a67fbfe8 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri May 25 00:36:54 2007 +0200 +++ b/src/HOL/IsaMakefile Fri May 25 05:18:56 2007 +0200 @@ -751,7 +751,7 @@ Nominal/Examples/ROOT.ML \ Nominal/Examples/CR.thy \ Nominal/Examples/CR_Takahashi.thy \ - Nominal/Examples/Class.thy \ +## Nominal/Examples/Class.thy \ Nominal/Examples/Compile.thy \ Nominal/Examples/Fsub.thy \ Nominal/Examples/Lambda_mu.thy \ diff -r f4779adcd1a2 -r 11e1a67fbfe8 src/HOL/Nominal/Examples/ROOT.ML --- a/src/HOL/Nominal/Examples/ROOT.ML Fri May 25 00:36:54 2007 +0200 +++ b/src/HOL/Nominal/Examples/ROOT.ML Fri May 25 05:18:56 2007 +0200 @@ -7,7 +7,7 @@ use_thy "CR"; use_thy "CR_Takahashi"; -use_thy "Class"; +(*use_thy "Class";*) use_thy "Compile"; use_thy "Fsub"; use_thy "Height";