| #
830577aa |
|
21-Jul-2018 |
paulson <lp15@cam.ac.uk> |
de-applying and removing junk
|
| #
b09a3f81 |
|
19-Jul-2018 |
paulson <lp15@cam.ac.uk> |
de-applying
|
| #
05d25f5b |
|
28-Jun-2018 |
nipkow <none@none> |
added lemmas
|
| #
a0960b42 |
|
28-Jun-2018 |
paulson <lp15@cam.ac.uk> |
Generalising and renaming some basic results
|
| #
8413f38b |
|
22-Jun-2018 |
wenzelm <none@none> |
clarified document antiquotation @{theory};
|
| #
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
| #
1387b04b |
|
19-Dec-2017 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
85b3e948 |
|
11-Nov-2017 |
haftmann <none@none> |
dedicated definition for coprimality
--HG--
extra : rebase_source : 891168c98ce62efae6b7e72c7d3365fea12b33ae
|
| #
8a74fa41 |
|
24-Oct-2017 |
immler <none@none> |
generalized lemmas cancelling real_of_int/real in (in)equalities with power; completed set of related simp rules; lemmas about floorlog/bitlen
|
| #
5c09067f |
|
09-Oct-2017 |
paulson <lp15@cam.ac.uk> |
new material about connectedness, etc.
|
| #
5ba2adde |
|
26-Aug-2017 |
nipkow <none@none> |
reorganized and added log-related lemmas
|
| #
2937a84f |
|
20-Jun-2017 |
haftmann <none@none> |
stripped code pre/postprocessor setup for real from superfluous rules
--HG--
extra : rebase_source : 913a617a752fa0c5ff08d04a724cd1023f2fb459
|
| #
4e651d44 |
|
21-May-2017 |
blanchet <none@none> |
added one more simplification to help replay
|
| #
351cc2e6 |
|
17-Oct-2016 |
nipkow <none@none> |
setsum -> sum
|
| #
d98e1fa1 |
|
29-Sep-2016 |
boehmes <none@none> |
invoke argo as part of the tried automatic proof methods
|
| #
eb8139dc |
|
29-Sep-2016 |
boehmes <none@none> |
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
|
| #
9b9c2176 |
|
12-Aug-2016 |
wenzelm <none@none> |
more symbols;
|
| #
372e3d05 |
|
05-Aug-2016 |
nipkow <none@none> |
added missing lemmas
|
| #
64974886 |
|
05-Aug-2016 |
nipkow <none@none> |
tuned floor lemmas
|
| #
b7ba6e77 |
|
15-Jul-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
| #
edfd8174 |
|
23-Jun-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
| #
13683eca |
|
17-Jun-2016 |
hoelzl <none@none> |
move Conditional_Complete_Lattices to Main
--HG--
extra : rebase_source : 2cd0f07680d0081b5d3769e8a4ad49983a312a99
|
| #
a2bc0021 |
|
25-Apr-2016 |
wenzelm <none@none> |
eliminated old 'def';
tuned comments;
|
| #
041061bc |
|
16-Mar-2016 |
paulson <lp15@cam.ac.uk> |
Contractible sets. Also removal of obsolete theorems and refactoring
|
| #
db1c38d3 |
|
15-Mar-2016 |
paulson <lp15@cam.ac.uk> |
rationalisation of theorem names esp about "real Archimedian" etc.
|
| #
15ee6658 |
|
24-Feb-2016 |
paulson <lp15@cam.ac.uk> |
Substantial new material for multivariate analysis. Also removal of some duplicates.
|
| #
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
| #
e3b38c13 |
|
17-Feb-2016 |
haftmann <none@none> |
dropped various legacy fact bindings
|
| #
a6f23363 |
|
17-Feb-2016 |
haftmann <none@none> |
generalized some lemmas;
moved some lemmas in more appropriate places;
deleted potentially dangerous simp rule
|
| #
5ad25152 |
|
05-Jan-2016 |
hoelzl <none@none> |
add the proof of the central limit theorem
--HG--
extra : rebase_source : 493d99e28392771c51f4102a11b90533880e289f
extra : amend_source : 3fb7b7c607104e57a2c3ba7f733dd570eb42fa3b
|
| #
227dc99e |
|
06-Jan-2016 |
blanchet <none@none> |
more complete setup for 'Rat' in Nitpick
|
| #
08cabf03 |
|
27-Dec-2015 |
wenzelm <none@none> |
prefer symbols for "abs";
|
| #
ecc07c37 |
|
27-Dec-2015 |
wenzelm <none@none> |
prefer symbols for "floor", "ceiling";
|
| #
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
53483153 |
|
16-Nov-2015 |
paulson <lp15@cam.ac.uk> |
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
|
| #
420aaf4c |
|
12-Nov-2015 |
paulson <lp15@cam.ac.uk> |
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
|
| #
3f106d8a |
|
10-Nov-2015 |
paulson <lp15@cam.ac.uk> |
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
|
| #
ae913163 |
|
30-Sep-2015 |
paulson <lp15@cam.ac.uk> |
real_of_nat_Suc is now a simprule
|
| #
33d48711 |
|
21-Sep-2015 |
paulson <none@none> |
new lemmas and movement of lemmas into place
|
| #
85ed9565 |
|
01-Sep-2015 |
wenzelm <none@none> |
eliminated \<Colon>;
|
| #
78ffd573 |
|
31-Aug-2015 |
wenzelm <none@none> |
prefer symbols;
|
| #
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
603f8dfb |
|
12-Jun-2015 |
haftmann <none@none> |
uniform _ div _ as infix syntax for ring division
--HG--
extra : rebase_source : c4a1892078772c7ce9af33ad66e2abfefe7adea9
|
| #
f2ba2c03 |
|
01-Jun-2015 |
haftmann <none@none> |
separate class for division operator, with particular syntax added in more specific classes
|
| #
d20797ec |
|
30-Apr-2015 |
paulson <lp15@cam.ac.uk> |
tidying some messy proofs
|
| #
9fdf6e80 |
|
09-Apr-2015 |
haftmann <none@none> |
conversion between division on nat/int and division in archmedean fields
|
| #
ac517014 |
|
31-Mar-2015 |
haftmann <none@none> |
given up separate type classes demanding `inverse 0 = 0`
|
| #
e54b5053 |
|
04-Mar-2015 |
nipkow <none@none> |
Removed the obsolete functions "natfloor" and "natceiling"
|
| #
ff53cb2b |
|
13-Nov-2014 |
hoelzl <none@none> |
import general theorems from AFP/Markov_Models
|
| #
374feb37 |
|
12-Nov-2014 |
immler <none@none> |
cancel real of power of numeral also for equality and strict inequality;
simplify floor of power of numeral;
lemmas about real/floor
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
dc5a029e |
|
30-Oct-2014 |
haftmann <none@none> |
more simp rules concerning dvd and even/odd
--HG--
extra : rebase_source : 895ed3f871c22790e8d199a30828e91bc13bd735
|
| #
9a196198 |
|
26-Oct-2014 |
hoelzl <none@none> |
further generalization of natfloor_div_nat
|
| #
71f7b745 |
|
26-Oct-2014 |
hoelzl <none@none> |
generalize natfloor_div_nat, add floor variant: floor_divide_real_eq_div
|
| #
1720153d |
|
02-Sep-2014 |
haftmann <none@none> |
more convenient printing of real numbers after evaluation
|
| #
53400fc4 |
|
29-Aug-2014 |
hoelzl <none@none> |
add simp rules for divisions of numerals in floor and ceiling.
--HG--
extra : rebase_source : ea537029d27222136caea445ff8f1f5f6c3ff58c
|
| #
ac75f5e7 |
|
27-Aug-2014 |
blanchet <none@none> |
renamed new SMT module from 'SMT2' to 'SMT'
--HG--
rename : src/HOL/SMT2.thy => src/HOL/SMT.thy
rename : src/HOL/Tools/SMT2/smt2_builtin.ML => src/HOL/Tools/SMT/smt_builtin.ML
rename : src/HOL/Tools/SMT2/smt2_config.ML => src/HOL/Tools/SMT/smt_config.ML
rename : src/HOL/Tools/SMT2/smt2_datatypes.ML => src/HOL/Tools/SMT/smt_datatypes.ML
rename : src/HOL/Tools/SMT2/smt2_failure.ML => src/HOL/Tools/SMT/smt_failure.ML
rename : src/HOL/Tools/SMT2/smt2_normalize.ML => src/HOL/Tools/SMT/smt_normalize.ML
rename : src/HOL/Tools/SMT2/smt2_real.ML => src/HOL/Tools/SMT/smt_real.ML
rename : src/HOL/Tools/SMT2/smt2_solver.ML => src/HOL/Tools/SMT/smt_solver.ML
rename : src/HOL/Tools/SMT2/smt2_systems.ML => src/HOL/Tools/SMT/smt_systems.ML
rename : src/HOL/Tools/SMT2/smt2_translate.ML => src/HOL/Tools/SMT/smt_translate.ML
rename : src/HOL/Tools/SMT2/smt2_util.ML => src/HOL/Tools/SMT/smt_util.ML
rename : src/HOL/Tools/SMT2/smtlib2.ML => src/HOL/Tools/SMT/smtlib.ML
rename : src/HOL/Tools/SMT2/smtlib2_interface.ML => src/HOL/Tools/SMT/smtlib_interface.ML
rename : src/HOL/Tools/SMT2/smtlib2_isar.ML => src/HOL/Tools/SMT/smtlib_isar.ML
rename : src/HOL/Tools/SMT2/smtlib2_proof.ML => src/HOL/Tools/SMT/smtlib_proof.ML
rename : src/HOL/Tools/SMT2/verit_isar.ML => src/HOL/Tools/SMT/verit_isar.ML
rename : src/HOL/Tools/SMT2/verit_proof.ML => src/HOL/Tools/SMT/verit_proof.ML
rename : src/HOL/Tools/SMT2/verit_proof_parse.ML => src/HOL/Tools/SMT/verit_proof_parse.ML
rename : src/HOL/Tools/SMT2/z3_new_interface.ML => src/HOL/Tools/SMT/z3_interface.ML
rename : src/HOL/Tools/SMT2/z3_new_isar.ML => src/HOL/Tools/SMT/z3_isar.ML
rename : src/HOL/Tools/SMT2/z3_new_proof.ML => src/HOL/Tools/SMT/z3_proof.ML
rename : src/HOL/Tools/SMT2/z3_new_real.ML => src/HOL/Tools/SMT/z3_real.ML
rename : src/HOL/Tools/SMT2/z3_new_replay.ML => src/HOL/Tools/SMT/z3_replay.ML
rename : src/HOL/Tools/SMT2/z3_new_replay_literals.ML => src/HOL/Tools/SMT/z3_replay_literals.ML
rename : src/HOL/Tools/SMT2/z3_new_replay_methods.ML => src/HOL/Tools/SMT/z3_replay_methods.ML
rename : src/HOL/Tools/SMT2/z3_new_replay_rules.ML => src/HOL/Tools/SMT/z3_replay_rules.ML
rename : src/HOL/Tools/SMT2/z3_new_replay_util.ML => src/HOL/Tools/SMT/z3_replay_util.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML => src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
rename : src/HOL/Word/Tools/smt2_word.ML => src/HOL/Word/Tools/smt_word.ML
|
| #
167005e9 |
|
27-Aug-2014 |
blanchet <none@none> |
moved old 'smt' method out of 'Main'
--HG--
rename : src/HOL/SMT.thy => src/HOL/Library/SMT.thy
rename : src/HOL/Tools/SMT/smt_builtin.ML => src/HOL/Library/SMT/smt_builtin.ML
rename : src/HOL/Tools/SMT/smt_config.ML => src/HOL/Library/SMT/smt_config.ML
rename : src/HOL/Tools/SMT/smt_datatypes.ML => src/HOL/Library/SMT/smt_datatypes.ML
rename : src/HOL/Tools/SMT/smt_failure.ML => src/HOL/Library/SMT/smt_failure.ML
rename : src/HOL/Tools/SMT/smt_normalize.ML => src/HOL/Library/SMT/smt_normalize.ML
rename : src/HOL/Tools/SMT/smt_real.ML => src/HOL/Library/SMT/smt_real.ML
rename : src/HOL/Tools/SMT/smt_setup_solvers.ML => src/HOL/Library/SMT/smt_setup_solvers.ML
rename : src/HOL/Tools/SMT/smt_solver.ML => src/HOL/Library/SMT/smt_solver.ML
rename : src/HOL/Tools/SMT/smt_translate.ML => src/HOL/Library/SMT/smt_translate.ML
rename : src/HOL/Tools/SMT/smt_utils.ML => src/HOL/Library/SMT/smt_utils.ML
rename : src/HOL/Tools/SMT/smtlib_interface.ML => src/HOL/Library/SMT/smtlib_interface.ML
rename : src/HOL/Tools/SMT/z3_interface.ML => src/HOL/Library/SMT/z3_interface.ML
rename : src/HOL/Tools/SMT/z3_model.ML => src/HOL/Library/SMT/z3_model.ML
rename : src/HOL/Tools/SMT/z3_proof_literals.ML => src/HOL/Library/SMT/z3_proof_literals.ML
rename : src/HOL/Tools/SMT/z3_proof_methods.ML => src/HOL/Library/SMT/z3_proof_methods.ML
rename : src/HOL/Tools/SMT/z3_proof_parser.ML => src/HOL/Library/SMT/z3_proof_parser.ML
rename : src/HOL/Tools/SMT/z3_proof_reconstruction.ML => src/HOL/Library/SMT/z3_proof_reconstruction.ML
rename : src/HOL/Tools/SMT/z3_proof_tools.ML => src/HOL/Library/SMT/z3_proof_tools.ML
|
| #
c5d3c38b |
|
25-Aug-2014 |
hoelzl <none@none> |
introduce real_of typeclass for real :: 'a => real
--HG--
extra : rebase_source : da71a0ef4d5378c1042d043ce015c1adae40b3f0
|
| #
d285560c |
|
19-Aug-2014 |
hoelzl <none@none> |
better linarith support for floor, ceiling, natfloor, and natceiling
--HG--
extra : rebase_source : fac55dc42162d71e9d329d10d498c370b963de40
|
| #
38907e37 |
|
05-Jul-2014 |
haftmann <none@none> |
prefer ac_simps collections over separate name bindings for add and mult
|
| #
e46c07fd |
|
04-Jul-2014 |
haftmann <none@none> |
reduced name variants for assoc and commute on plus and mult
|
| #
6c0336e5 |
|
30-Jun-2014 |
hoelzl <none@none> |
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
--HG--
extra : rebase_source : 03b2468f7b324b9d8add229ae59776b447283141
|
| #
58c27ade |
|
17-Jun-2014 |
hoelzl <none@none> |
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
--HG--
extra : rebase_source : cd4a9d91f2d415deaa6fd3411b5402ef770d74d2
|
| #
61aadd1e |
|
06-May-2014 |
hoelzl <none@none> |
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
--HG--
extra : rebase_source : 899541490c73fe6897445f97dc2a5a3c929cf153
|
| #
66804330 |
|
14-Apr-2014 |
hoelzl <none@none> |
added divide_nonneg_nonneg and co; made it a simp rule
--HG--
extra : rebase_source : 998eadb7cfbf8720cf961ac2e149ce4537557a47
|
| #
5723122d |
|
12-Apr-2014 |
nipkow <none@none> |
made mult_pos_pos a simp rule
|
| #
838cbeac |
|
11-Apr-2014 |
nipkow <none@none> |
made divide_pos_pos a simp rule
|
| #
a444e184 |
|
11-Apr-2014 |
nipkow <none@none> |
made mult_nonneg_nonneg a simp rule
--HG--
extra : rebase_source : 3f70ac991fa0f02839309ce9b8f418ff53f87c36
|
| #
956719cb |
|
19-Mar-2014 |
paulson <lp15@cam.ac.uk> |
Some rationalisation of basic lemmas
|
| #
6b4f08d8 |
|
13-Mar-2014 |
blanchet <none@none> |
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
|
| #
b9ba5739 |
|
06-Mar-2014 |
blanchet <none@none> |
renamed 'fun_rel' to 'rel_fun'
|
| #
ac866a0f |
|
25-Dec-2013 |
haftmann <none@none> |
prefer more canonical names for lemmas on min/max
|
| #
138816de |
|
19-Nov-2013 |
haftmann <none@none> |
eliminiated neg_numeral in favour of - (numeral _)
|
| #
dddd44d5 |
|
05-Nov-2013 |
hoelzl <none@none> |
int and nat are conditionally_complete_lattices
--HG--
extra : rebase_source : 4295ba08a6a68dc20cc2a24971781ce06b986aac
|
| #
839a96d8 |
|
05-Nov-2013 |
hoelzl <none@none> |
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
--HG--
rename : src/HOL/Library/Glbs.thy => src/HOL/Library/Lubs_Glbs.thy
|
| #
f77e220a |
|
05-Nov-2013 |
hoelzl <none@none> |
generalize bdd_above/below_uminus to ordered_ab_group_add
|
| #
19339e2f |
|
05-Nov-2013 |
hoelzl <none@none> |
use bdd_above and bdd_below for conditionally complete lattices
|
| #
d2ef840a |
|
01-Nov-2013 |
haftmann <none@none> |
more simplification rules on unary and binary minus
--HG--
extra : rebase_source : 7c88c9f33c4be8eae76f508a1a73ba79c8b769b1
|
| #
837093ba |
|
16-Sep-2013 |
kuncar <none@none> |
use lifting_forget for deregistering numeric types as a quotient type
|
| #
7237bdd9 |
|
02-Sep-2013 |
wenzelm <none@none> |
tuned proofs -- clarified flow of facts wrt. calculation;
|
| #
b9bb5600 |
|
18-Aug-2013 |
wenzelm <none@none> |
more symbols;
|
| #
8c36fedb |
|
13-May-2013 |
kuncar <none@none> |
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
|
| #
812b19ed |
|
25-Apr-2013 |
hoelzl <none@none> |
revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
|
| #
09075f4b |
|
24-Apr-2013 |
hoelzl <none@none> |
spell conditional_ly_-complete lattices correct
--HG--
rename : src/HOL/Conditional_Complete_Lattices.thy => src/HOL/Conditionally_Complete_Lattices.thy
extra : rebase_source : fe25f4dff8edab189f8c7a631785ba3cc5a19aa2
|
| #
adb29bd9 |
|
25-Mar-2013 |
hoelzl <none@none> |
rename RealDef to Real
|
| #
e41352e0 |
|
25-Mar-2013 |
hoelzl <none@none> |
remove Real.thy
|
| #
ed30ca3e |
|
25-Mar-2013 |
hoelzl <none@none> |
merge RComplete into RealDef
|
| #
e3227796 |
|
22-Aug-2012 |
wenzelm <none@none> |
prefer ML_file over old uses;
|
| #
5d3ecda1 |
|
12-May-2010 |
boehmes <none@none> |
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
|
| #
b033a7b7 |
|
10-Feb-2010 |
haftmann <none@none> |
moved lemma field_le_epsilon from Real.thy to Fields.thy
|
| #
1df0dfbe |
|
09-Feb-2010 |
haftmann <none@none> |
simple proofs make life faster and easier
|
| #
5d17693c |
|
05-Feb-2010 |
haftmann <none@none> |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
| #
0b210e9b |
|
05-Oct-2009 |
paulson <none@none> |
New lemmas connected with the reals and infinite series
|
| #
66194568 |
|
29-Dec-2008 |
haftmann <none@none> |
adapted HOL source structure to distribution layout
--HG--
rename : src/HOL/Library/Dense_Linear_Order.thy => src/HOL/Dense_Linear_Order.thy
rename : src/HOL/Complex/Fundamental_Theorem_Algebra.thy => src/HOL/Fundamental_Theorem_Algebra.thy
rename : src/HOL/Real/HahnBanach/Bounds.thy => src/HOL/HahnBanach/Bounds.thy
rename : src/HOL/Real/HahnBanach/FunctionNorm.thy => src/HOL/HahnBanach/FunctionNorm.thy
rename : src/HOL/Real/HahnBanach/FunctionOrder.thy => src/HOL/HahnBanach/FunctionOrder.thy
rename : src/HOL/Real/HahnBanach/HahnBanach.thy => src/HOL/HahnBanach/HahnBanach.thy
rename : src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy => src/HOL/HahnBanach/HahnBanachExtLemmas.thy
rename : src/HOL/Real/HahnBanach/HahnBanachLemmas.thy => src/HOL/HahnBanach/HahnBanachLemmas.thy
rename : src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy => src/HOL/HahnBanach/HahnBanachSupLemmas.thy
rename : src/HOL/Real/HahnBanach/Linearform.thy => src/HOL/HahnBanach/Linearform.thy
rename : src/HOL/Real/HahnBanach/NormedSpace.thy => src/HOL/HahnBanach/NormedSpace.thy
rename : src/HOL/Real/HahnBanach/README.html => src/HOL/HahnBanach/README.html
rename : src/HOL/Real/HahnBanach/ROOT.ML => src/HOL/HahnBanach/ROOT.ML
rename : src/HOL/Real/HahnBanach/Subspace.thy => src/HOL/HahnBanach/Subspace.thy
rename : src/HOL/Real/HahnBanach/VectorSpace.thy => src/HOL/HahnBanach/VectorSpace.thy
rename : src/HOL/Real/HahnBanach/ZornLemma.thy => src/HOL/HahnBanach/ZornLemma.thy
rename : src/HOL/Real/HahnBanach/document/root.bib => src/HOL/HahnBanach/document/root.bib
rename : src/HOL/Real/HahnBanach/document/root.tex => src/HOL/HahnBanach/document/root.tex
rename : src/HOL/Real/RealVector.thy => src/HOL/RealVector.thy
rename : src/HOL/Hyperreal/SEQ.thy => src/HOL/SEQ.thy
|
| #
ba08d3a4 |
|
11-Dec-2008 |
nipkow <none@none> |
codegen
|
| #
7fe13fce |
|
10-Dec-2008 |
nipkow <none@none> |
moved ContNotDenum into Library
--HG--
rename : src/HOL/ContNotDenum.thy => src/HOL/Library/ContNotDenum.thy
|
| #
f21befe1 |
|
03-Dec-2008 |
haftmann <none@none> |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
--HG--
rename : src/HOL/Library/Code_Message.thy => src/HOL/Code_Message.thy
rename : src/HOL/Complex/Complex.thy => src/HOL/Complex.thy
rename : src/HOL/Complex/Complex_Main.thy => src/HOL/Complex_Main.thy
rename : src/HOL/Real/ContNotDenum.thy => src/HOL/ContNotDenum.thy
rename : src/HOL/Hyperreal/Deriv.thy => src/HOL/Deriv.thy
rename : src/HOL/Hyperreal/Fact.thy => src/HOL/Fact.thy
rename : src/HOL/Hyperreal/FrechetDeriv.thy => src/HOL/FrechetDeriv.thy
rename : src/HOL/Library/GCD.thy => src/HOL/GCD.thy
rename : src/HOL/Hyperreal/Integration.thy => src/HOL/Integration.thy
rename : src/HOL/Real/Float.thy => src/HOL/Library/Float.thy
rename : src/HOL/Hyperreal/Lim.thy => src/HOL/Lim.thy
rename : src/HOL/Hyperreal/Ln.thy => src/HOL/Ln.thy
rename : src/HOL/Hyperreal/Log.thy => src/HOL/Log.thy
rename : src/HOL/Real/Lubs.thy => src/HOL/Lubs.thy
rename : src/HOL/Hyperreal/MacLaurin.thy => src/HOL/MacLaurin.thy
rename : src/HOL/Hyperreal/NthRoot.thy => src/HOL/NthRoot.thy
rename : src/HOL/Library/Order_Relation.thy => src/HOL/Order_Relation.thy
rename : src/HOL/Real/PReal.thy => src/HOL/PReal.thy
rename : src/HOL/Library/Parity.thy => src/HOL/Parity.thy
rename : src/HOL/Real/RComplete.thy => src/HOL/RComplete.thy
rename : src/HOL/Real/Rational.thy => src/HOL/Rational.thy
rename : src/HOL/Real/Real.thy => src/HOL/Real.thy
rename : src/HOL/Real/RealDef.thy => src/HOL/RealDef.thy
rename : src/HOL/Real/RealPow.thy => src/HOL/RealPow.thy
rename : src/HOL/Hyperreal/Series.thy => src/HOL/Series.thy
rename : src/HOL/Hyperreal/Taylor.thy => src/HOL/Taylor.thy
rename : src/HOL/arith_data.ML => src/HOL/Tools/arith_data.ML
rename : src/HOL/Real/float_arith.ML => src/HOL/Tools/float_arith.ML
rename : src/HOL/Real/float_syntax.ML => src/HOL/Tools/float_syntax.ML
rename : src/HOL/hologic.ML => src/HOL/Tools/hologic.ML
rename : src/HOL/int_arith1.ML => src/HOL/Tools/int_arith.ML
rename : src/HOL/int_factor_simprocs.ML => src/HOL/Tools/int_factor_simprocs.ML
rename : src/HOL/nat_simprocs.ML => src/HOL/Tools/nat_simprocs.ML
rename : src/HOL/Real/rat_arith.ML => src/HOL/Tools/rat_arith.ML
rename : src/HOL/Real/real_arith.ML => src/HOL/Tools/real_arith.ML
rename : src/HOL/simpdata.ML => src/HOL/Tools/simpdata.ML
rename : src/HOL/Hyperreal/Transcendental.thy => src/HOL/Transcendental.thy
rename : src/HOL/Library/RType.thy => src/HOL/Typerep.thy
rename : src/HOL/Library/Univ_Poly.thy => src/HOL/Univ_Poly.thy
rename : src/HOL/Complex/ex/Arithmetic_Series_Complex.thy => src/HOL/ex/Arithmetic_Series_Complex.thy
rename : src/HOL/Complex/ex/BigO_Complex.thy => src/HOL/ex/BigO_Complex.thy
rename : src/HOL/Complex/ex/HarmonicSeries.thy => src/HOL/ex/HarmonicSeries.thy
rename : src/HOL/Complex/ex/MIR.thy => src/HOL/ex/MIR.thy
rename : src/HOL/Complex/ex/ReflectedFerrack.thy => src/HOL/ex/ReflectedFerrack.thy
rename : src/HOL/Complex/ex/Sqrt.thy => src/HOL/ex/Sqrt.thy
rename : src/HOL/Complex/ex/Sqrt_Script.thy => src/HOL/ex/Sqrt_Script.thy
rename : src/HOL/Complex/ex/linrtac.ML => src/HOL/ex/linrtac.ML
rename : src/HOL/Complex/ex/mirtac.ML => src/HOL/ex/mirtac.ML
rename : src/Pure/Tools/quickcheck.ML => src/Tools/quickcheck.ML
rename : src/Pure/Tools/value.ML => src/Tools/value.ML
|