equal
deleted
inserted
replaced
8 theory Import_Setup |
8 theory Import_Setup |
9 imports Main |
9 imports Main |
10 keywords "import_type_map" "import_const_map" "import_file" :: thy_decl |
10 keywords "import_type_map" "import_const_map" "import_file" :: thy_decl |
11 begin |
11 begin |
12 |
12 |
13 ML_file "import_data.ML" |
13 ML_file \<open>import_data.ML\<close> |
14 |
14 |
15 lemma light_ex_imp_nonempty: |
15 lemma light_ex_imp_nonempty: |
16 "P t \<Longrightarrow> \<exists>x. x \<in> Collect P" |
16 "P t \<Longrightarrow> \<exists>x. x \<in> Collect P" |
17 by auto |
17 by auto |
18 |
18 |
24 |
24 |
25 lemma ext2: |
25 lemma ext2: |
26 "(\<And>x. f x = g x) \<Longrightarrow> f = g" |
26 "(\<And>x. f x = g x) \<Longrightarrow> f = g" |
27 by auto |
27 by auto |
28 |
28 |
29 ML_file "import_rule.ML" |
29 ML_file \<open>import_rule.ML\<close> |
30 |
30 |
31 end |
31 end |
32 |
32 |