2004-01-08 kleing 2004-01-08 separate thm lists in latex output by \isasep
2004-01-08 kleing 2004-01-08 run makeindex if necessary
2004-01-07 kleing 2004-01-07 map_idI
2004-01-06 paulson 2004-01-06 auto update
2004-01-06 paulson 2004-01-06 Ring_and_Field now requires axiom add_left_imp_eq for semirings. This allows more theorems to be proved for semirings, but requires a redundant axiom to be proved for rings, etc.
2004-01-06 paulson 2004-01-06 correction to cterm_instantiate by Christoph Leuth
2004-01-05 nipkow 2004-01-05 *** empty log message ***
2004-01-05 nipkow 2004-01-05 *** empty log message ***
2004-01-05 nipkow 2004-01-05 undid split_comp_eq[simp] because it leads to nontermination together with split_def!
2004-01-03 paulson 2004-01-03 Deleting more redundant theorems
2004-01-01 paulson 2004-01-01 conversion of Real/PReal to Isar script; type "complex" is now in class "field"
2004-01-01 paulson 2004-01-01 tweaking of lemmas in RealDef, RealOrd
2003-12-29 kleing 2003-12-29 \<^bsub> .. \<^esub>
2003-12-29 kleing 2003-12-29 spanning super and sub scripts \<^bsub> .. \<^esub> and \<^bsup> .. \<^esup>
2003-12-27 paulson 2003-12-27 re-organized numeric lemmas
2003-12-25 nipkow 2003-12-25 Added trace msg
2003-12-25 paulson 2003-12-25 re-organized some hyperreal and real lemmas
2003-12-24 kleing 2003-12-24 list_all2_nthD no good as [intro?]
2003-12-23 kleing 2003-12-23 list_all2_mono should not be [trans]
2003-12-23 paulson 2003-12-23 reorganised complex arithmetic
2003-12-23 paulson 2003-12-23 removing real_of_posnat
2003-12-23 paulson 2003-12-23 converting Hyperreal/NthRoot to Isar
2003-12-23 paulson 2003-12-23 converting Complex/Complex.ML to Isar
2003-12-23 paulson 2003-12-23 deleting redundant theorems
2003-12-23 paulson 2003-12-23 new theorems
2003-12-23 paulson 2003-12-23 tidying up hcomplex arithmetic
2003-12-23 paulson 2003-12-23 renaming some theorems
2003-12-23 paulson 2003-12-23 type hcomplex is now in class field
2003-12-23 paulson 2003-12-23 more ML bindings
2003-12-23 kleing 2003-12-23 added some [intro?] and [trans] for list_all2 lemmas
2003-12-22 nipkow 2003-12-22 Updated proofs due to changes in Set.thy.
2003-12-22 paulson 2003-12-22 converted Complex/NSComplex to Isar script
2003-12-22 paulson 2003-12-22 removal of the abel_cancel simproc for hypreal
2003-12-22 paulson 2003-12-22 downgrading abel_cancel
2003-12-22 paulson 2003-12-22 new binding
2003-12-22 paulson 2003-12-22 simplifying
2003-12-22 paulson 2003-12-22 moving HyperArith0.ML to other theories
2003-12-22 paulson 2003-12-22 removing obsolete bindings
2003-12-21 paulson 2003-12-21 tidying of HOL/Auth esp Guard lemmas
2003-12-21 nipkow 2003-12-21 removed insert_Diff_single from simpset because it interfered with Auth :-(
2003-12-19 paulson 2003-12-19 tidying first part of HyperArith0.ML, using generic lemmas
2003-12-19 paulson 2003-12-19 minor tweaks
2003-12-19 paulson 2003-12-19 type hypreal is an ordered field
2003-12-19 nipkow 2003-12-19 *** empty log message ***
2003-12-18 paulson 2003-12-18 tidied
2003-12-18 nipkow 2003-12-18 *** empty log message ***
2003-12-17 paulson 2003-12-17 converted Hyperreal/HyperDef to Isar script
2003-12-16 kleing 2003-12-16 fixed PG link
2003-12-16 paulson 2003-12-16 converted Hyperreal/HyperOrd to new-style theory
2003-12-15 paulson 2003-12-15 updated references to the now-pornographic proofgeneral.org
2003-12-15 paulson 2003-12-15 more general lemmas for Ring_and_Field
2003-12-13 paulson 2003-12-13 absolute value theorems moved to HOL/Ring_and_Field
2003-12-12 paulson 2003-12-12 moving some division theorems to Ring_and_Field
2003-12-12 kleing 2003-12-12 changed proof general links
2003-12-11 ballarin 2003-12-11 Change to prune_prems in Pure/Isar/locale.ML.
2003-12-11 paulson 2003-12-11 removal of abel_cancel from Real
2003-12-10 paulson 2003-12-10 combining Real/{RealArith0,real_arith}.ML
2003-12-10 paulson 2003-12-10 Moving some theorems from Real/RealArith0.ML
2003-12-10 ballarin 2003-12-10 Isar: where attribute supports instantiation of type variables.
2003-12-10 ballarin 2003-12-10 New structure "partial_object" as common root for lattices and magmas.