# HG changeset patch # User desharna # Date 1742315077 -3600 # Tue Mar 18 17:24:37 2025 +0100 # Node ID 49c3d5537ff6e29e972b67575f6e7346ffc18515 # Parent 717a35a21348956e082bb198bf4289dd74994a2f removed debug command diff --git a/thys/Superposition_Calculus/Ground_Superposition_Welltypedness_Preservation.thy b/thys/Superposition_Calculus/Ground_Superposition_Welltypedness_Preservation.thy --- a/thys/Superposition_Calculus/Ground_Superposition_Welltypedness_Preservation.thy +++ b/thys/Superposition_Calculus/Ground_Superposition_Welltypedness_Preservation.thy @@ -9,12 +9,6 @@ sublocale ground_typing where \<F> = "\<F> :: ('f, 'ty) fun_types" . -term clause.is_welltyped -(* -"clause.is_welltyped" - :: "'f gterm uprod literal multiset \<Rightarrow> bool" -*) - context fixes \<F> :: "('f, 'ty) fun_types" begin