Removed a wrongly committed unfinished (cheated) theorem...

HOL-Theorem-Prover · Sep 27, 2023 · ec242fa · ec242fa
1 parent 48c784c
commit ec242fa
Showing 1 changed file with 0 additions and 7 deletions.
diff --git a/examples/lambda/barendregt/solvableScript.sml b/examples/lambda/barendregt/solvableScript.sml
@@ -482,13 +482,6 @@ Proof
  >> Q.EXISTS_TAC ‘Ns'’ >> rw []
 QED
 
-(* Theorem 8.3.3 (ii) *)
-Theorem solvable_iff_solvable_LAM :
-    !M x. solvable M <=> solvable (LAM x M)
-Proof
-    cheat
-QED
-
 val _ = export_theory ();
 val _ = html_theory "solvable";