Mercurial Mercurial > repos > isabelle / annotate
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/Complex_Main.thy
author paulson <lp15@cam.ac.uk>
Mon, 03 Jul 2023 11:45:59 +0100
changeset 78248 740b23f1138a
parent 73411 1f1366966296
child 80177 1478555580af
permissions -rw-r--r--
EXPERIMENTAL replacement of f ` A <= B by f : A -> B in Analysis
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset 
     1
 
section \<open>Comprehensive Complex Theory\<close>
13984
e055ba9020eb new theory Complex_Main as basis for analysis developments
paulson
parents:
diff changeset 
     2
 







15131






c69542757a4d
New theory header syntax.



nipkow


parents: 
13984

diff
changeset




     3


theory Complex_Main








27472






47bc28e011d5
removed nonstandard analysis theories to HOL-NSA



huffman


parents: 
27368

diff
changeset




     4


imports








29879






4425849f5db7
Moved FTA into Lib and cleaned it up a little.



nipkow


parents: 
29304

diff
changeset




     5


  Complex








63570






1826a90b9cbc
simplified theory structure;



wenzelm


parents: 
60758

diff
changeset




     6


  MacLaurin








15131






c69542757a4d
New theory header syntax.



nipkow


parents: 
13984

diff
changeset




     7


begin








13984






e055ba9020eb
new theory Complex_Main as basis for analysis developments



paulson


parents: 

diff
changeset




     8









73411






1f1366966296
avoid name clash



haftmann


parents: 
63571

diff
changeset




     9


end














isabelle