2004-04-14 kleing [Wed, 14 Apr 2004 14:13:05 +0200] rev 14565
use more symbols in HTML output
src/CTT/CTT.thy src/FOL/IFOL.thy src/HOL/Finite_Set.thy src/HOL/Fun.thy src/HOL/HOL.thy src/HOL/Hyperreal/HyperDef.thy src/HOL/Hyperreal/IntFloor.thy src/HOL/Hyperreal/NSA.thy src/HOL/IMP/Compiler0.thy src/HOL/IMP/Machines.thy src/HOL/IMP/Natural.thy src/HOL/IMP/Transition.thy src/HOL/Induct/QuoDataType.thy src/HOL/Infinite_Set.thy src/HOL/Lambda/Type.thy src/HOL/Library/FuncSet.thy src/HOL/Library/Nat_Infinity.thy src/HOL/Library/Word.thy src/HOL/List.thy src/HOL/NanoJava/Equivalence.thy src/HOL/Product_Type.thy src/HOL/Real/HahnBanach/VectorSpace.thy src/HOL/Set.thy src/HOL/TLA/Intensional.thy src/HOL/TLA/TLA.thy src/HOL/Transitive_Closure.thy src/HOLCF/IOA/meta_theory/Pred.thy src/HOLCF/Sprod0.thy src/HOLCF/Ssum0.thy src/Pure/Thy/html.ML src/Sequents/LK0.thy src/ZF/Cardinal.thy src/ZF/CardinalArith.thy src/ZF/Integ/Int.thy src/ZF/Main.thy src/ZF/OrdQuant.thy src/ZF/Ordinal.thy src/ZF/ZF.thy

2004-04-14 wenzelm [Wed, 14 Apr 2004 13:28:46 +0200] rev 14564
renamed have_thms to note_thms;
src/Pure/Isar/calculation.ML src/Pure/Isar/isar_thy.ML src/Pure/Isar/locale.ML src/Pure/Isar/proof.ML src/Pure/Isar/proof_context.ML src/Pure/pure_thy.ML

2004-04-14 wenzelm [Wed, 14 Apr 2004 13:26:27 +0200] rev 14563
tuned;
src/Pure/Isar/args.ML

2004-04-14 wenzelm [Wed, 14 Apr 2004 13:25:51 +0200] rev 14562
proper handling of lines terminated by CRLF or CR;
src/Pure/General/symbol.ML

2004-04-14 schirmer [Wed, 14 Apr 2004 12:19:16 +0200] rev 14561
* raw control symbols are of the form \<^raw:...> now.
* again allowing symbols to begin with "\\" instead of "\" for
compatibility with ML-strings of old style theory and ML-files and
isa-ProofGeneral.
NEWS src/Pure/General/symbol.ML src/Pure/Thy/latex.ML src/Pure/proof_general.ML

2004-04-14 berghofe [Wed, 14 Apr 2004 11:44:57 +0200] rev 14560
Fixed bug in check_mode_clause.
src/HOL/Tools/inductive_codegen.ML

2004-04-14 schirmer [Wed, 14 Apr 2004 10:08:28 +0200] rev 14559
bugfix for \<^raw...> scanner
src/Pure/General/symbol.ML

2004-04-14 kleing [Wed, 14 Apr 2004 09:53:25 +0200] rev 14558
prod and sum
src/Pure/Thy/html.ML

2004-04-13 schirmer [Tue, 13 Apr 2004 23:08:12 +0200] rev 14557
* cleaner distinction between control symbols "\<^...>" and "\<^raw...>" in
the scanner
* output functions default_output and xsymbols_output
only print one "\" for symbols (to be consistent with the scanner).
src/Pure/General/symbol.ML src/Pure/proof_general.ML

2004-04-13 wenzelm [Tue, 13 Apr 2004 20:31:55 +0200] rev 14556
* Calculation commands "moreover" and "also" no longer interfere with
current facts ("this"), admitting arbitrary combinations with "then"
and derived forms.
NEWS