2008-03-20 wenzelm [Thu, 20 Mar 2008 00:20:44 +0100] rev 26343
simplified get_thm(s): back to plain name argument;
src/FOL/ex/LocaleTest.thy src/HOL/Import/proof_kernel.ML src/HOL/Matrix/cplex/matrixlp.ML src/HOL/Modelcheck/mucke_oracle.ML src/HOL/Nominal/nominal_atoms.ML src/HOL/Nominal/nominal_fresh_fun.ML src/HOL/Nominal/nominal_inductive.ML src/HOL/Nominal/nominal_package.ML src/HOL/Nominal/nominal_permeq.ML src/HOL/Nominal/nominal_thmdecls.ML src/HOL/Statespace/distinct_tree_prover.ML src/HOL/Statespace/state_space.ML src/HOL/Tools/datatype_package.ML src/HOL/Tools/datatype_rep_proofs.ML src/HOL/Tools/inductive_realizer.ML src/HOLCF/IOA/meta_theory/ioa_package.ML src/HOLCF/Tools/domain/domain_theorems.ML src/HOLCF/Tools/fixrec_package.ML src/Pure/Proof/extraction.ML src/Pure/ProofGeneral/proof_general_pgip.ML src/Tools/Compute_Oracle/linker.ML

2008-03-19 wenzelm [Wed, 19 Mar 2008 22:50:42 +0100] rev 26342
more antiquotations;
src/CCL/CCL.thy src/CCL/Term.thy src/CCL/Type.thy src/FOL/ex/Classical.thy src/FOL/ex/Miniscope.thy src/HOL/Algebra/abstract/Ideal2.thy src/HOL/Algebra/abstract/Ring2.thy src/HOL/Algebra/poly/LongDiv.thy src/HOL/Auth/Message.thy src/HOL/Bali/AxExample.thy src/HOL/Bali/AxSem.thy src/HOL/Bali/Example.thy src/HOL/Fun.thy src/HOL/HoareParallel/Gar_Coll.thy src/HOL/HoareParallel/Mul_Gar_Coll.thy src/HOL/IMP/VC.thy src/HOL/IOA/Solve.thy src/HOL/MicroJava/J/Conform.thy src/HOL/Modelcheck/EindhovenSyn.thy src/HOL/Modelcheck/MuckeSyn.thy src/HOL/Modelcheck/mucke_oracle.ML src/HOL/NatBin.thy src/HOL/Nominal/Nominal.thy src/HOL/SET-Protocol/MessageSET.thy src/HOL/TLA/Buffer/DBuffer.thy src/HOL/TLA/Inc/Inc.thy src/HOL/TLA/Memory/MemClerk.thy src/HOL/TLA/Memory/Memory.thy src/HOL/TLA/Memory/MemoryImplementation.thy src/HOL/TLA/Memory/RPC.thy src/HOL/W0/W0.thy src/HOLCF/IOA/ABP/Correctness.thy src/HOLCF/Tools/domain/domain_theorems.ML

2008-03-19 wenzelm [Wed, 19 Mar 2008 22:47:39 +0100] rev 26341
avoid Auto_tac;
src/HOL/Tools/cnf_funcs.ML

2008-03-19 wenzelm [Wed, 19 Mar 2008 22:47:38 +0100] rev 26340
more antiquotations;
eliminated change_claset/simpset;
src/HOL/Product_Type.thy src/HOL/Transitive_Closure.thy

2008-03-19 wenzelm [Wed, 19 Mar 2008 22:47:35 +0100] rev 26339
eliminated change_claset/simpset;
src/HOL/Datatype.thy src/HOL/Set.thy src/HOLCF/HOLCF.thy src/HOLCF/IOA/NTP/Correctness.thy src/HOLCF/IOA/meta_theory/CompoTraces.thy src/HOLCF/IOA/meta_theory/TLS.thy src/HOLCF/IOA/meta_theory/Traces.thy src/ZF/Main_ZF.thy src/ZF/OrdQuant.thy

2008-03-19 wenzelm [Wed, 19 Mar 2008 22:28:17 +0100] rev 26338
auxiliary dynamic_thm(s) for fact lookup;
renamed local dynamic_thm(s) to goal_thm(s);
src/HOL/Nominal/nominal_permeq.ML

2008-03-19 wenzelm [Wed, 19 Mar 2008 22:28:08 +0100] rev 26337
auxiliary dynamic_thm(s) for fact lookup;
src/HOL/Nominal/nominal_atoms.ML src/HOL/Nominal/nominal_fresh_fun.ML src/HOL/Nominal/nominal_inductive.ML src/HOL/Nominal/nominal_package.ML src/HOL/Nominal/nominal_thmdecls.ML

2008-03-19 wenzelm [Wed, 19 Mar 2008 22:27:57 +0100] rev 26336
renamed datatype thmref to Facts.ref, tuned interfaces;
src/FOL/ex/LocaleTest.thy src/HOL/Import/proof_kernel.ML src/HOL/Matrix/cplex/matrixlp.ML src/HOL/Modelcheck/mucke_oracle.ML src/HOL/Statespace/distinct_tree_prover.ML src/HOL/Statespace/state_space.ML src/HOL/Tools/datatype_package.ML src/HOL/Tools/datatype_rep_proofs.ML src/HOL/Tools/inductive_package.ML src/HOL/Tools/inductive_realizer.ML src/HOL/Tools/inductive_set_package.ML src/HOL/Tools/recdef_package.ML src/HOLCF/IOA/meta_theory/ioa_package.ML src/HOLCF/Tools/domain/domain_theorems.ML src/HOLCF/Tools/fixrec_package.ML src/Pure/Isar/args.ML src/Pure/Isar/attrib.ML src/Pure/Isar/calculation.ML src/Pure/Isar/element.ML src/Pure/Isar/find_theorems.ML src/Pure/Isar/isar_cmd.ML src/Pure/Isar/proof.ML src/Pure/Isar/proof_context.ML src/Pure/Isar/proof_display.ML src/Pure/Isar/spec_parse.ML src/Pure/Isar/specification.ML src/Pure/ML/ml_context.ML src/Pure/Proof/extraction.ML src/Pure/ProofGeneral/proof_general_pgip.ML src/Pure/facts.ML src/Pure/pure_thy.ML src/Tools/Compute_Oracle/linker.ML src/Tools/code/code_package.ML src/ZF/Tools/datatype_package.ML src/ZF/Tools/induct_tacs.ML src/ZF/Tools/inductive_package.ML

2008-03-19 wenzelm [Wed, 19 Mar 2008 18:15:25 +0100] rev 26335
removed redundant Nat.less_not_sym, Nat.less_asym;
renamed Nat.less_irrefl to less_irrefl_nat, no longer declared elim;
NEWS src/HOL/Nat.thy

2008-03-19 wenzelm [Wed, 19 Mar 2008 18:15:13 +0100] rev 26334
removed redundant Nat.less_irrefl;
src/HOL/ex/Primrec.thy src/HOLCF/ex/Hoare.thy