# HG changeset patch
# User wenzelm
# Date 1737025952 -3600
# Node ID b93e6b458433d87384f42e70ef2e4e4cfaf39894
# Parent  9755a8921fbc56e860df62ef39df36a69f054c1c
tuned proofs;

diff -r 9755a8921fbc -r b93e6b458433 src/HOL/Import/Import_Setup.thy
--- a/src/HOL/Import/Import_Setup.thy	Thu Jan 16 11:55:20 2025 +0100
+++ b/src/HOL/Import/Import_Setup.thy	Thu Jan 16 12:12:32 2025 +0100
@@ -12,19 +12,16 @@
 
 ML_file \<open>import_data.ML\<close>
 
-lemma light_ex_imp_nonempty:
-  "P t \<Longrightarrow> \<exists>x. x \<in> Collect P"
+lemma light_ex_imp_nonempty: "P t \<Longrightarrow> \<exists>x. x \<in> Collect P"
   by auto
 
 lemma typedef_hol2hollight:
-  assumes a: "type_definition Rep Abs (Collect P)"
-  shows "Abs (Rep a) = a \<and> P r = (Rep (Abs r) = r)"
+  "type_definition Rep Abs (Collect P) \<Longrightarrow> Abs (Rep a) = a \<and> P r = (Rep (Abs r) = r)"
   by (metis type_definition.Rep_inverse type_definition.Abs_inverse
-      type_definition.Rep a mem_Collect_eq)
+      type_definition.Rep mem_Collect_eq)
 
-lemma ext2:
-  "(\<And>x. f x = g x) \<Longrightarrow> f = g"
-  by auto
+lemma ext2: "(\<And>x. f x = g x) \<Longrightarrow> f = g"
+  by (rule ext)
 
 ML_file \<open>import_rule.ML\<close>