src/HOL/Prolog/Test.thy
changeset 46473 a687b75f9fa8
parent 42793 88bee9f6eec7
child 51311 337cfc42c9c8
     1.1 --- a/src/HOL/Prolog/Test.thy	Tue Feb 14 21:31:26 2012 +0100
     1.2 +++ b/src/HOL/Prolog/Test.thy	Tue Feb 14 21:45:32 2012 +0100
     1.3 @@ -270,11 +270,5 @@
     1.4    apply (prolog prog_Test)
     1.5    back
     1.6    done
     1.7 -(*
     1.8 -back
     1.9 --> problem with DEPTH_SOLVE:
    1.10 -Exception- THM ("dest_state", 1, ["P x & P y --> P y"]) raised
    1.11 -Exception raised at run-time
    1.12 -*)
    1.13  
    1.14  end