--- a/src/HOL/Finite_Set.thy Fri Aug 17 09:20:45 2007 +0200
+++ b/src/HOL/Finite_Set.thy Fri Aug 17 13:58:57 2007 +0200
@@ -2424,7 +2424,6 @@
have ne: "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
have "\<Sqinter>(insert x A) \<squnion> \<Sqinter>B = (x \<sqinter> \<Sqinter>A) \<squnion> \<Sqinter>B"
using insert
- thm ACIf.fold1_insert_idem_def
by(simp add:ACIf.fold1_insert_idem_def[OF ACIf_inf Inf_def])
also have "\<dots> = (x \<squnion> \<Sqinter>B) \<sqinter> (\<Sqinter>A \<squnion> \<Sqinter>B)" by(rule sup_inf_distrib2)
also have "\<dots> = \<Sqinter>{x \<squnion> b|b. b \<in> B} \<sqinter> \<Sqinter>{a \<squnion> b|a b. a \<in> A \<and> b \<in> B}"
--- a/src/HOL/Set.thy Fri Aug 17 09:20:45 2007 +0200
+++ b/src/HOL/Set.thy Fri Aug 17 13:58:57 2007 +0200
@@ -147,7 +147,6 @@
instance set :: (type) ord
subset_def: "A \<le> B \<equiv> \<forall>x\<in>A. x \<in> B"
psubset_def: "A < B \<equiv> A \<le> B \<and> A \<noteq> B" ..
-
lemmas [code func del] = subset_def psubset_def
abbreviation
--- a/src/Pure/Isar/theory_target.ML Fri Aug 17 09:20:45 2007 +0200
+++ b/src/Pure/Isar/theory_target.ML Fri Aug 17 13:58:57 2007 +0200
@@ -163,7 +163,7 @@
in
-fun defs loc kind args lthy0 =
+fun defs kind args lthy0 =
let
fun def ((c, mx), ((name, atts), rhs)) lthy1 =
let
@@ -350,7 +350,7 @@
consts = consts is_loc some_class,
axioms = axioms,
abbrev = abbrev is_loc some_class,
- defs = defs loc,
+ defs = defs,
notes = notes loc,
type_syntax = type_syntax loc,
term_syntax = term_syntax loc,