2001-01-09 nipkow [Tue, 09 Jan 2001 15:36:30 +0100] rev 10835
` -> $
src/HOLCF/IMP/Denotational.ML src/HOLCF/IMP/Denotational.thy src/HOLCF/IMP/HoareEx.thy src/HOLCF/IOA/meta_theory/Abstraction.ML src/HOLCF/IOA/meta_theory/Abstraction.thy src/HOLCF/IOA/meta_theory/CompoExecs.ML src/HOLCF/IOA/meta_theory/CompoExecs.thy src/HOLCF/IOA/meta_theory/CompoScheds.ML src/HOLCF/IOA/meta_theory/CompoScheds.thy src/HOLCF/IOA/meta_theory/CompoTraces.ML src/HOLCF/IOA/meta_theory/CompoTraces.thy src/HOLCF/IOA/meta_theory/Compositionality.ML src/HOLCF/IOA/meta_theory/Deadlock.ML src/HOLCF/IOA/meta_theory/LiveIOA.thy src/HOLCF/IOA/meta_theory/RefCorrectness.ML src/HOLCF/IOA/meta_theory/RefCorrectness.thy src/HOLCF/IOA/meta_theory/RefMappings.thy src/HOLCF/IOA/meta_theory/Seq.ML src/HOLCF/IOA/meta_theory/Seq.thy src/HOLCF/IOA/meta_theory/Sequence.ML src/HOLCF/IOA/meta_theory/Sequence.thy src/HOLCF/IOA/meta_theory/ShortExecutions.ML src/HOLCF/IOA/meta_theory/ShortExecutions.thy src/HOLCF/IOA/meta_theory/SimCorrectness.ML src/HOLCF/IOA/meta_theory/SimCorrectness.thy src/HOLCF/IOA/meta_theory/Simulations.ML src/HOLCF/IOA/meta_theory/Simulations.thy src/HOLCF/IOA/meta_theory/TL.ML src/HOLCF/IOA/meta_theory/TL.thy src/HOLCF/IOA/meta_theory/TLS.ML src/HOLCF/IOA/meta_theory/TLS.thy src/HOLCF/IOA/meta_theory/Traces.ML src/HOLCF/IOA/meta_theory/Traces.thy src/HOLCF/domain/theorems.ML src/HOLCF/ex/Dagstuhl.thy src/HOLCF/ex/Dnat.ML src/HOLCF/ex/Dnat.thy src/HOLCF/ex/Fix2.ML src/HOLCF/ex/Fix2.thy src/HOLCF/ex/Focus_ex.ML src/HOLCF/ex/Focus_ex.thy src/HOLCF/ex/Hoare.ML src/HOLCF/ex/Hoare.thy src/HOLCF/ex/Loop.ML src/HOLCF/ex/Loop.thy src/HOLCF/ex/Stream.ML src/HOLCF/ex/loeckx.ML

2001-01-09 nipkow [Tue, 09 Jan 2001 15:32:27 +0100] rev 10834
*** empty log message ***
src/HOL/Hyperreal/HRealAbs.ML src/HOL/Hyperreal/HSeries.ML src/HOL/Hyperreal/HSeries.thy src/HOL/Hyperreal/HyperDef.ML src/HOL/Hyperreal/HyperDef.thy src/HOL/Hyperreal/HyperNat.ML src/HOL/Hyperreal/HyperNat.thy src/HOL/Hyperreal/HyperPow.ML src/HOL/Hyperreal/HyperPow.thy src/HOL/Hyperreal/Lim.ML src/HOL/Hyperreal/NSA.ML src/HOL/Hyperreal/NatStar.ML src/HOL/Hyperreal/NatStar.thy src/HOL/Hyperreal/SEQ.ML src/HOL/Hyperreal/Star.ML src/HOL/Hyperreal/Star.thy src/HOL/IMPP/Hoare.ML src/HOL/IMPP/Hoare.thy src/HOL/Induct/LList.ML src/HOL/Induct/LList.thy src/HOL/Integ/Equiv.ML src/HOL/Integ/Equiv.thy src/HOL/Integ/IntDef.ML src/HOL/Integ/IntDef.thy src/HOL/Integ/int_arith1.ML src/HOL/Lattice/Bounds.thy src/HOL/Lattice/CompleteLattice.thy src/HOL/Lattice/Orders.thy src/HOL/Lex/Automata.ML src/HOL/Lex/Automata.thy src/HOL/Lex/NA.thy src/HOL/Lex/NAe.ML src/HOL/Lex/NAe.thy src/HOL/Lex/RegExp2NA.thy src/HOL/Lex/RegExp2NAe.thy src/HOL/MicroJava/BV/JVM.thy src/HOL/MicroJava/J/JBasis.ML src/HOL/NumberTheory/BijectionRel.ML src/HOL/NumberTheory/EulerFermat.ML src/HOL/NumberTheory/EulerFermat.thy src/HOL/NumberTheory/WilsonBij.ML src/HOL/Real/PNat.ML src/HOL/Real/PNat.thy src/HOL/Real/PRat.ML src/HOL/Real/PRat.thy src/HOL/Real/PReal.ML src/HOL/Real/RealDef.ML src/HOL/Real/RealDef.thy src/HOL/Real/RealInt.ML src/HOL/Real/RealInt.thy ...

2001-01-09 nipkow [Tue, 09 Jan 2001 15:29:17 +0100] rev 10833
`` -> ` and ``` -> ``
src/HOL/Algebra/abstract/Ideal.ML src/HOL/Auth/KerberosIV.ML src/HOL/Auth/Kerberos_BAN.ML src/HOL/Auth/Message.ML src/HOL/Auth/Message.thy src/HOL/Auth/NS_Shared.ML src/HOL/Auth/OtwayRees.ML src/HOL/Auth/OtwayRees_AN.ML src/HOL/Auth/OtwayRees_Bad.ML src/HOL/Auth/Public.ML src/HOL/Auth/Public.thy src/HOL/Auth/Recur.ML src/HOL/Auth/Shared.ML src/HOL/Auth/Shared.thy src/HOL/Auth/TLS.ML src/HOL/Auth/Yahalom.ML src/HOL/Auth/Yahalom2.ML src/HOL/Auth/Yahalom_Bad.ML

2001-01-09 nipkow [Tue, 09 Jan 2001 15:22:13 +0100] rev 10832
`` -> and ``` -> ``
src/HOL/Datatype_Universe.thy src/HOL/Finite.ML src/HOL/Fun.ML src/HOL/Inverse_Image.ML src/HOL/Inverse_Image.thy src/HOL/List.ML src/HOL/List.thy src/HOL/NatDef.ML src/HOL/NatDef.thy src/HOL/Product_Type.ML src/HOL/Relation.ML src/HOL/Relation.thy src/HOL/Set.ML src/HOL/Set.thy src/HOL/Sum_Type.thy src/HOL/Wellfounded_Recursion.ML src/HOL/equalities.ML src/HOL/mono.ML

2001-01-09 wenzelm [Tue, 09 Jan 2001 15:18:07 +0100] rev 10831
replaced \<macron> by \<inverse>;
src/Pure/Thy/html.ML

2001-01-09 wenzelm [Tue, 09 Jan 2001 15:17:08 +0100] rev 10830
avoid renaming of params in cases;
src/Pure/Isar/proof.ML src/Pure/Isar/proof_context.ML src/Pure/Isar/rule_cases.ML

2001-01-09 wenzelm [Tue, 09 Jan 2001 15:15:28 +0100] rev 10829
split_all operation;
src/HOL/Product_Type.ML

2001-01-09 oheimb [Tue, 09 Jan 2001 13:54:44 +0100] rev 10828
improved evaluation judgment syntax; modified Loop rule
src/HOL/MicroJava/J/Eval.thy src/HOL/MicroJava/J/JBasis.ML src/HOL/MicroJava/J/JTypeSafe.ML

2001-01-09 wenzelm [Tue, 09 Jan 2001 12:11:56 +0100] rev 10827
syntax (xsymbols);
src/HOL/Transitive_Closure.thy

2001-01-08 nipkow [Mon, 08 Jan 2001 12:27:36 +0100] rev 10826
Removed Applyall
src/HOL/Fun.ML src/HOL/Fun.thy