2009-11-24 haftmann [Tue, 24 Nov 2009 17:28:25 +0100] rev 33955
curried take/drop
src/FOLP/simp.ML src/HOL/Import/hol4rews.ML src/HOL/Modelcheck/MuckeSyn.thy src/HOL/Modelcheck/mucke_oracle.ML src/HOL/Nominal/nominal_datatype.ML src/HOL/Nominal/nominal_induct.ML src/HOL/Tools/Datatype/datatype.ML src/HOL/Tools/Datatype/datatype_abs_proofs.ML src/HOL/Tools/Datatype/datatype_codegen.ML src/HOL/Tools/Datatype/datatype_prop.ML src/HOL/Tools/Datatype/datatype_rep_proofs.ML src/HOL/Tools/Function/fun.ML src/HOL/Tools/Groebner_Basis/groebner.ML src/HOL/Tools/Nitpick/nitpick.ML src/HOL/Tools/Nitpick/nitpick_scope.ML src/HOL/Tools/TFL/tfl.ML src/HOL/Tools/inductive.ML src/HOL/Tools/inductive_realizer.ML src/HOL/Tools/old_primrec.ML src/HOL/Tools/record.ML src/HOL/Tools/refute.ML src/HOL/Tools/split_rule.ML src/HOLCF/Tools/Domain/domain_extender.ML src/Provers/splitter.ML src/Pure/General/path.ML src/Pure/General/scan.ML src/Pure/General/symbol.ML src/Pure/Isar/code.ML src/Pure/Isar/obtain.ML src/Pure/Isar/proof_context.ML src/Pure/Isar/rule_cases.ML src/Pure/Proof/extraction.ML src/Pure/Syntax/ast.ML src/Pure/Syntax/syntax.ML src/Pure/Thy/present.ML src/Pure/Thy/thy_output.ML src/Pure/Tools/find_theorems.ML src/Pure/assumption.ML src/Pure/codegen.ML src/Pure/goal_display.ML src/Pure/library.ML src/Pure/meta_simplifier.ML src/Pure/proofterm.ML src/Pure/tactic.ML src/Pure/thm.ML src/Pure/variable.ML src/Tools/Code/code_haskell.ML src/Tools/Code/code_printer.ML src/Tools/Code/code_thingol.ML src/Tools/induct.ML ...

2009-11-24 haftmann [Tue, 24 Nov 2009 14:37:23 +0100] rev 33954
backported parts of abstract byte code verifier from AFP/Jinja
src/HOL/IsaMakefile src/HOL/MicroJava/BV/Altern.thy src/HOL/MicroJava/BV/BVExample.thy src/HOL/MicroJava/BV/BVNoTypeError.thy src/HOL/MicroJava/BV/BVSpec.thy src/HOL/MicroJava/BV/BVSpecTypeSafe.thy src/HOL/MicroJava/BV/Correct.thy src/HOL/MicroJava/BV/Effect.thy src/HOL/MicroJava/BV/EffectMono.thy src/HOL/MicroJava/BV/Err.thy src/HOL/MicroJava/BV/JType.thy src/HOL/MicroJava/BV/JVM.thy src/HOL/MicroJava/BV/JVMType.thy src/HOL/MicroJava/BV/Kildall.thy src/HOL/MicroJava/BV/LBVComplete.thy src/HOL/MicroJava/BV/LBVCorrect.thy src/HOL/MicroJava/BV/LBVJVM.thy src/HOL/MicroJava/BV/LBVSpec.thy src/HOL/MicroJava/BV/Listn.thy src/HOL/MicroJava/BV/Opt.thy src/HOL/MicroJava/BV/Product.thy src/HOL/MicroJava/BV/Semilat.thy src/HOL/MicroJava/BV/SemilatAlg.thy src/HOL/MicroJava/BV/Typing_Framework.thy src/HOL/MicroJava/BV/Typing_Framework_JVM.thy src/HOL/MicroJava/BV/Typing_Framework_err.thy src/HOL/MicroJava/Comp/AuxLemmas.thy src/HOL/MicroJava/Comp/CorrComp.thy src/HOL/MicroJava/Comp/CorrCompTp.thy src/HOL/MicroJava/Comp/DefsComp.thy src/HOL/MicroJava/Comp/Index.thy src/HOL/MicroJava/Comp/LemmasComp.thy src/HOL/MicroJava/Comp/NatCanonify.thy src/HOL/MicroJava/Comp/TranslComp.thy src/HOL/MicroJava/Comp/TranslCompTp.thy src/HOL/MicroJava/Comp/TypeInf.thy src/HOL/MicroJava/DFA/Abstract_BV.thy src/HOL/MicroJava/DFA/Err.thy src/HOL/MicroJava/DFA/Kildall.thy src/HOL/MicroJava/DFA/LBVComplete.thy src/HOL/MicroJava/DFA/LBVCorrect.thy src/HOL/MicroJava/DFA/LBVSpec.thy src/HOL/MicroJava/DFA/Listn.thy src/HOL/MicroJava/DFA/Opt.thy src/HOL/MicroJava/DFA/Product.thy src/HOL/MicroJava/DFA/Semilat.thy src/HOL/MicroJava/DFA/SemilatAlg.thy src/HOL/MicroJava/DFA/Semilattices.thy src/HOL/MicroJava/DFA/Typing_Framework.thy src/HOL/MicroJava/DFA/Typing_Framework_err.thy ...

2009-12-04 wenzelm [Fri, 04 Dec 2009 14:21:07 +0100] rev 33953
added document_node;
tuned comments;
src/Pure/General/xml.scala

2009-12-04 wenzelm [Fri, 04 Dec 2009 12:17:38 +0100] rev 33952
document init_component shell function;
doc-src/System/Thy/Basics.thy doc-src/System/Thy/document/Basics.tex

2009-12-04 wenzelm [Fri, 04 Dec 2009 11:44:57 +0100] rev 33951
back to after-release mode;
CONTRIBUTORS NEWS

2009-12-04 wenzelm [Fri, 04 Dec 2009 11:41:17 +0100] rev 33950
back to main repository;
Admin/makedist

2009-12-04 wenzelm [Fri, 04 Dec 2009 11:19:00 +0100] rev 33949
merged

2009-12-04 haftmann [Fri, 04 Dec 2009 11:04:07 +0100] rev 33948
merged

2009-12-04 haftmann [Fri, 04 Dec 2009 11:03:54 +0100] rev 33947
added Crude_Executable_Set
src/HOL/Library/Crude_Executable_Set.thy

2009-12-04 nipkow [Fri, 04 Dec 2009 08:52:09 +0100] rev 33946
removed redundant lemma
src/HOL/GCD.thy src/HOL/Number_Theory/Primes.thy