src/FOL/ex/Classical.thy
changeset 36319 8feb2c4bef1a
parent 32960 69916a850301
child 42789 3a84b6947932
     1.1 --- a/src/FOL/ex/Classical.thy	Fri Apr 23 23:33:48 2010 +0200
     1.2 +++ b/src/FOL/ex/Classical.thy	Fri Apr 23 23:35:43 2010 +0200
     1.3 @@ -363,7 +363,7 @@
     1.4  
     1.5  text{*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
     1.6    fast DISCOVERS who killed Agatha. *}
     1.7 -lemma "lives(agatha) & lives(butler) & lives(charles) &  
     1.8 +schematic_lemma "lives(agatha) & lives(butler) & lives(charles) &  
     1.9     (killed(agatha,agatha) | killed(butler,agatha) | killed(charles,agatha)) &  
    1.10     (\<forall>x y. killed(x,y) --> hates(x,y) & ~richer(x,y)) &  
    1.11     (\<forall>x. hates(agatha,x) --> ~hates(charles,x)) &