Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Set.thy
changeset 61378 3e04c9ca001a
parent 61306 9dd394c866fc
child 61518 ff12606337e9 
--- a/src/HOL/Set.thy	Fri Oct 09 19:51:20 2015 +0200
+++ b/src/HOL/Set.thy	Fri Oct 09 20:26:03 2015 +0200
@@ -33,12 +33,6 @@
   not_member  ("op \<notin>") and
   not_member  ("(_/ \<notin> _)" [51, 51] 50)
 
-notation (HTML output)
-  member      ("op \<in>") and
-  member      ("(_/ \<in> _)" [51, 51] 50) and
-  not_member  ("op \<notin>") and
-  not_member  ("(_/ \<notin> _)" [51, 51] 50)
-
 
 text \<open>Set comprehensions\<close>
 
@@ -167,12 +161,6 @@
   subset_eq  ("op \<subseteq>") and
   subset_eq  ("(_/ \<subseteq> _)" [51, 51] 50)
 
-notation (HTML output)
-  subset  ("op \<subset>") and
-  subset  ("(_/ \<subset> _)" [51, 51] 50) and
-  subset_eq  ("op \<subseteq>") and
-  subset_eq  ("(_/ \<subseteq> _)" [51, 51] 50)
-
 abbreviation (input)
   supset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   "supset \<equiv> greater"
@@ -210,11 +198,6 @@
   "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)
   "_Bleast"     :: "id => 'a set => bool => 'a"           ("(3LEAST_\<in>_./ _)" [0, 0, 10] 10)
 
-syntax (HTML output)
-  "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
-  "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
-  "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)
-
 translations
   "ALL x:A. P" == "CONST Ball A (%x. P)"
   "EX x:A. P" == "CONST Bex A (%x. P)"
@@ -242,13 +225,6 @@
   "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3? _<=_./ _)" [0, 0, 10] 10)
   "_setleEx1"   :: "[idt, 'a, bool] => bool"   ("(3?! _<=_./ _)" [0, 0, 10] 10)
 
-syntax (HTML output)
-  "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subset>_./ _)"  [0, 0, 10] 10)
-  "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subset>_./ _)"  [0, 0, 10] 10)
-  "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10)
-  "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
-  "_setleEx1"   :: "[idt, 'a, bool] => bool"   ("(3\<exists>!_\<subseteq>_./ _)" [0, 0, 10] 10)
-
 translations
  "\<forall>A\<subset>B. P"   =>  "ALL A. A \<subset> B --> P"
  "\<exists>A\<subset>B. P"   =>  "EX A. A \<subset> B & P"
@@ -701,9 +677,6 @@
 notation (xsymbols)
   inter  (infixl "\<inter>" 70)
 
-notation (HTML output)
-  inter  (infixl "\<inter>" 70)
-
 lemma Int_def:
   "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
   by (simp add: inf_set_def inf_fun_def)
@@ -735,9 +708,6 @@
 notation (xsymbols)
   union  (infixl "\<union>" 65)
 
-notation (HTML output)
-  union  (infixl "\<union>" 65)
-
 lemma Un_def:
   "A \<union> B = {x. x \<in> A \<or> x \<in> B}"
   by (simp add: sup_set_def sup_fun_def)
isabelle