thys/Simplifying.thy
changeset 286 804fbb227568
parent 283 c4d821c6309d
child 293 1a4e5b94293b
--- a/thys/Simplifying.thy	Wed May 16 20:58:39 2018 +0100
+++ b/thys/Simplifying.thy	Wed Aug 15 13:48:57 2018 +0100
@@ -230,7 +230,7 @@
    qed
  qed  
 
-
+(*
 fun simp2_ALT where
   "simp2_ALT ZERO r2 seen = (r2, seen)"
 | "simp2_ALT r1 ZERO seen = (r1, seen)"
@@ -367,5 +367,5 @@
    apply(simp add: Sequ_def)
    apply(auto)[1]
   oops  
-
+*)
 end
\ No newline at end of file