src/HOL/Metis_Examples/Clausification.thy
changeset 47308 9caab698dbe4
parent 43228 2ed2f092e990
child 50696 85f944352d55
     1.1 --- a/src/HOL/Metis_Examples/Clausification.thy	Tue Apr 03 14:09:37 2012 +0200
     1.2 +++ b/src/HOL/Metis_Examples/Clausification.thy	Tue Apr 03 16:26:48 2012 +0200
     1.3 @@ -131,7 +131,7 @@
     1.4  by (metis bounded_def subset_eq)
     1.5  
     1.6  lemma
     1.7 -  assumes a: "Quotient R Abs Rep"
     1.8 +  assumes a: "Quotient R Abs Rep T"
     1.9    shows "symp R"
    1.10  using a unfolding Quotient_def using sympI
    1.11  by (metis (full_types))