# HG changeset patch
# User krauss
# Date 1300738229 -3600
# Node ID 1eda69f0b9a8305c3e59d523843cac42d12432e3
# Parent  f90040058a24edc07c18adee41f8603125f69dd4
moved some configurations to AFP, and fixed others

diff -r f90040058a24 -r 1eda69f0b9a8 Admin/mira.py
--- a/Admin/mira.py	Mon Mar 21 17:14:52 2011 +0100
+++ b/Admin/mira.py	Mon Mar 21 21:10:29 2011 +0100
@@ -294,21 +294,11 @@
     return (some_success, '', data, raw_attachments, None)
 
 
-@configuration(repos = [Isabelle, AFP], deps = [(HOL, [0])])
-def JD_Arrow(*args):
-    """Judgement Day regression suite Arrow"""
-    return judgement_day('Afp/thys/ArrowImpossibilityGS/Thys', 'Arrow_Order', 'prover_timeout=10', *args)
-
 @configuration(repos = [Isabelle], deps = [(HOL, [0])])
 def JD_NS(*args):
     """Judgement Day regression suite NS"""
     return judgement_day('Isabelle/src/HOL/Auth', 'NS_Shared', 'prover_timeout=10', *args)
 
-@configuration(repos = [Isabelle, AFP], deps = [(HOL, [0])])
-def JD_FFT(*args):
-    """Judgement Day regression suite FFT"""
-    return judgement_day('Afp/thys/FFT', 'FFT', 'prover_timeout=10', *args)
-
 @configuration(repos = [Isabelle], deps = [(HOL, [0])])
 def JD_FTA(*args):
     """Judgement Day regression suite FTA"""
@@ -317,25 +307,10 @@
 @configuration(repos = [Isabelle], deps = [(HOL, [0])])
 def JD_Hoare(*args):
     """Judgement Day regression suite Hoare"""
-    return judgement_day('Isabelle/src/HOL/IMP', 'Hoare', 'prover_timeout=10', *args)
-
-@configuration(repos = [Isabelle, AFP], deps = [(HOL, [0])])
-def JD_Jinja(*args):
-    """Judgement Day regression suite Jinja"""
-    return judgement_day('Afp/thys/Jinja/J', 'TypeSafe', 'prover_timeout=10', *args)
+    return judgement_day('Isabelle/src/HOL/IMPP', 'Hoare', 'prover_timeout=10', *args)
 
 @configuration(repos = [Isabelle], deps = [(HOL, [0])])
 def JD_SN(*args):
     """Judgement Day regression suite SN"""
-    return judgement_day('Isabelle/src/HOL/Lambda', 'StrongNorm', 'prover_timeout=10', *args)
+    return judgement_day('Isabelle/src/HOL/Proofs/Lambda', 'StrongNorm', 'prover_timeout=10', *args)
 
-@configuration(repos = [Isabelle, AFP], deps = [(HOL, [0])])
-def JD_QE(*args):
-    """Judgement Day regression suite QE"""
-    return judgement_day('Afp/thys/LinearQuantifierElim/Thys', 'QEpres', 'prover_timeout=10', *args)
-
-@configuration(repos = [Isabelle, AFP], deps = [(HOL, [0])])
-def JD_S2S(*args):
-    """Judgement Day regression suite S2S"""
-    return judgement_day('Afp/thys/SumSquares', 'TwoSquares', 'prover_timeout=10', *args)
-