--- 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>