changeset 11635  fd242f857508 
parent 11591  4b171ad4ff65 
child 14981  e73f8140af78 
11634:cddf6441a14a  11635:fd242f857508 

50 proof 
50 proof 
51 assume "?P = ?Q" 
51 assume "?P = ?Q" 
52 hence "Eps ?P = Eps ?Q" by (rule arg_cong) 
52 hence "Eps ?P = Eps ?Q" by (rule arg_cong) 
53 also note P 
53 also note P 
54 also note Q 
54 also note Q 
55 finally have "False = True" . 
55 finally show False by (rule False_neq_True) 
56 thus False by (rule False_neq_True) 

57 qed 
56 qed 
58 have "\<not> A" 
57 have "\<not> A" 
59 proof 
58 proof 
60 assume a: A 
59 assume a: A 
61 have "?P = ?Q" 
60 have "?P = ?Q" 