src/HOL/ex/Classical.thy
changeset 36319 8feb2c4bef1a
parent 32960 69916a850301
child 41959 b460124855b8
     1.1 --- a/src/HOL/ex/Classical.thy	Fri Apr 23 23:33:48 2010 +0200
     1.2 +++ b/src/HOL/ex/Classical.thy	Fri Apr 23 23:35:43 2010 +0200
     1.3 @@ -348,7 +348,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) &