Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Backed out changeset: a8ad7f6dd217---bypassing Main breaks theories that use \<inf> or \<sup>
authortraytel
Fri, 29 Nov 2013 14:24:21 +0100
changeset 54612 7e291ae244ea
parent 54611 31afce809794
child 54613 985f8b49c050
Backed out changeset: a8ad7f6dd217---bypassing Main breaks theories that use \<inf> or \<sup>
src/HOL/Library/Infinite_Set.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Infinite_Set.thy	Fri Nov 29 08:26:45 2013 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Fri Nov 29 14:24:21 2013 +0100
@@ -5,7 +5,7 @@
 header {* Infinite Sets and Related Concepts *}
 
 theory Infinite_Set
-imports Set_Interval
+imports Main
 begin
 
 subsection "Infinite Sets"
@@ -554,3 +554,4 @@
   by (simp add: atmost_one_def)
 
 end
+
isabelle