1.1 --- a/Admin/mira.py	Mon Mar 21 17:14:52 2011 +0100
     1.2 +++ b/Admin/mira.py	Mon Mar 21 21:10:29 2011 +0100
     1.3 @@ -294,21 +294,11 @@
     1.4      return (some_success, '', data, raw_attachments, None)
     1.5  
     1.6  
     1.7 -@configuration(repos = [Isabelle, AFP], deps = [(HOL, [0])])
     1.8 -def JD_Arrow(*args):
     1.9 -    """Judgement Day regression suite Arrow"""
    1.10 -    return judgement_day('Afp/thys/ArrowImpossibilityGS/Thys', 'Arrow_Order', 'prover_timeout=10', *args)
    1.11 -
    1.12  @configuration(repos = [Isabelle], deps = [(HOL, [0])])
    1.13  def JD_NS(*args):
    1.14      """Judgement Day regression suite NS"""
    1.15      return judgement_day('Isabelle/src/HOL/Auth', 'NS_Shared', 'prover_timeout=10', *args)
    1.16  
    1.17 -@configuration(repos = [Isabelle, AFP], deps = [(HOL, [0])])
    1.18 -def JD_FFT(*args):
    1.19 -    """Judgement Day regression suite FFT"""
    1.20 -    return judgement_day('Afp/thys/FFT', 'FFT', 'prover_timeout=10', *args)
    1.21 -
    1.22  @configuration(repos = [Isabelle], deps = [(HOL, [0])])
    1.23  def JD_FTA(*args):
    1.24      """Judgement Day regression suite FTA"""
    1.25 @@ -317,25 +307,10 @@
    1.26  @configuration(repos = [Isabelle], deps = [(HOL, [0])])
    1.27  def JD_Hoare(*args):
    1.28      """Judgement Day regression suite Hoare"""
    1.29 -    return judgement_day('Isabelle/src/HOL/IMP', 'Hoare', 'prover_timeout=10', *args)
    1.30 -
    1.31 -@configuration(repos = [Isabelle, AFP], deps = [(HOL, [0])])
    1.32 -def JD_Jinja(*args):
    1.33 -    """Judgement Day regression suite Jinja"""
    1.34 -    return judgement_day('Afp/thys/Jinja/J', 'TypeSafe', 'prover_timeout=10', *args)
    1.35 +    return judgement_day('Isabelle/src/HOL/IMPP', 'Hoare', 'prover_timeout=10', *args)
    1.36  
    1.37  @configuration(repos = [Isabelle], deps = [(HOL, [0])])
    1.38  def JD_SN(*args):
    1.39      """Judgement Day regression suite SN"""
    1.40 -    return judgement_day('Isabelle/src/HOL/Lambda', 'StrongNorm', 'prover_timeout=10', *args)
    1.41 +    return judgement_day('Isabelle/src/HOL/Proofs/Lambda', 'StrongNorm', 'prover_timeout=10', *args)
    1.42  
    1.43 -@configuration(repos = [Isabelle, AFP], deps = [(HOL, [0])])
    1.44 -def JD_QE(*args):
    1.45 -    """Judgement Day regression suite QE"""
    1.46 -    return judgement_day('Afp/thys/LinearQuantifierElim/Thys', 'QEpres', 'prover_timeout=10', *args)
    1.47 -
    1.48 -@configuration(repos = [Isabelle, AFP], deps = [(HOL, [0])])
    1.49 -def JD_S2S(*args):
    1.50 -    """Judgement Day regression suite S2S"""
    1.51 -    return judgement_day('Afp/thys/SumSquares', 'TwoSquares', 'prover_timeout=10', *args)
    1.52 -