Hi again, thanks to all contributors who already started to sort out some of the set-pred mixture issues.
I have merged recent changes back into http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/ -- this is meant as a mere basis for figuring out problems experimentally, not as a proper history to be taken over finally! Currently makeall says: HOL-ex FAILED HOL-Decision_Procs FAILED HOL-Nominal FAILED HOL-Bali FAILED HOL-Hoare_Parallel FAILED HOLCF-Library FAILED HOL-Induct FAILED HOL-Library FAILED HOL-Metis_Examples FAILED HOL-MicroJava FAILED HOL-NanoJava FAILED HOL-Nitpick_Examples FAILED HOL-Quotient_Examples FAILED HOL-Predicate_Compile_Examples FAILED HOL-Word-SMT_Examples FAILED HOL-Subst FAILED HOL-TPTP FAILED HOL-Multivariate_Analysis FAILED HOL-IMP FAILED Possible showstoppers: haftmann@macbroy20:~/data/isabelle/with_set$ grep -rIPl 'Collect_def|mem_def' src/HOL/*/ src/HOL/Library/Predicate_Compile_Alternative_Defs.thy src/HOL/Library/Executable_Set.thy src/HOL/Library/Cset.thy src/HOL/Library/More_Set.thy src/HOL/Library/List_Cset.thy src/HOL/Quotient_Examples/FSet.thy src/HOL/Quotient_Examples/List_Cset.thy src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy src/HOL/Nitpick_Examples/Core_Nits.thy src/HOL/Nominal/Examples/Standardization.thy src/HOL/Nominal/Nominal.thy src/HOL/TPTP/CASC_Setup.thy src/HOL/SMT_Examples/SMT_Tests.thy src/HOL/MicroJava/J/TypeRel.thy src/HOL/MicroJava/BV/BVExample.thy src/HOL/Metis_Examples/Message.thy src/HOL/Metis_Examples/Tarski.thy src/HOL/Metis_Examples/Trans_Closure.thy src/HOL/Metis_Examples/Sets.thy src/HOL/Metis_Examples/Proxies.thy src/HOL/Metis_Examples/Abstraction.thy A glimpse at the AFP: haftmann@macbroy20:~/data/isabelle/afp/blank$ grep -rIPl 'Collect_def|mem_def' thys/ thys/HRB-Slicing/JinjaVM_Inter/JVMInterpretation.thy thys/Group-Ring-Module/Algebra1.thy thys/FinFun/FinFunSet.thy thys/FinFun/FinFun.thy thys/Slicing/JinjaVM/SemanticsWF.thy.orig thys/LinearQuantifierElim/Thys/QE.thy thys/DataRefinementIBP/Diagram.thy thys/DataRefinementIBP/DataRefinement.thy thys/DataRefinementIBP/Preliminaries.thy thys/Tree-Automata/Ta_impl.thy thys/Lower_Semicontinuous/Lower_Semicontinuous.thy thys/Flyspeck-Tame/LowerBound.thy thys/Flyspeck-Tame/ScoreProps.thy thys/JinjaThreads/BV/BCVExec.thy thys/JinjaThreads/MM/Orders.thy thys/JinjaThreads/MM/JMM_Spec.thy thys/JinjaThreads/Execute/ExternalCall_Execute.thy thys/JinjaThreads/Execute/JVMExec_Execute.thy thys/JinjaThreads/Execute/JVM_Execute2.thy thys/JinjaThreads/Execute/TypeRelRefine.thy thys/JinjaThreads/Common/SemiType.thy thys/JinjaThreads/Common/Cset_Monad.thy thys/JinjaThreads/Common/Aux.thy thys/JinjaThreads/Compiler/PCompiler.thy thys/JinjaThreads/Compiler/JVMJ1.thy thys/JinjaThreads/Compiler/Execs.thy thys/JinjaThreads/Framework/LTS.thy thys/JinjaThreads/Framework/FWLTS.thy thys/JinjaThreads/Framework/FWDeadlock.thy thys/JinjaThreads/Framework/FWBisimDeadlock.thy thys/JinjaThreads/Framework/FWBisimulation.thy thys/JinjaThreads/Framework/Bisimulation.thy thys/Coinductive/Coinductive_Nat.thy thys/Coinductive/TLList.thy thys/Coinductive/Coinductive_List_Lib.thy thys/Binomial-Heaps/SkewBinomialHeap.thy thys/Perfect-Number-Thm/Sigma.thy thys/GraphMarkingIBP/DSWMark.thy thys/GraphMarkingIBP/Preliminaries.thy thys/GraphMarkingIBP/LinkMark.thy thys/GraphMarkingIBP/StackMark.thy thys/POPLmark-deBruijn/Execute.thy thys/Shivers-CFA/ExCFSV.thy thys/Shivers-CFA/HOLCFUtils.thy thys/Abstract-Rewriting/Abstract_Rewriting.thy thys/Presburger-Automata/Presburger_Automata.thy thys/Presburger-Automata/DFS.thy thys/Collections/ListSetImpl.thy thys/Collections/common/FTGAAdd.thy thys/Collections/AnnotatedListGAPrioUniqueImpl.thy thys/NormByEval/NBE.thy thys/Free-Groups/Isomorphisms.thy thys/KBPs/DFS.thy thys/SIFPL/VS.thy thys/SIFPL/VS_OBJ.thy thys/SIFPL/HuntSands.thy thys/ArrowImpossibilityGS/Thys/Arrow_Order.thy A vast area for volunteers. Cheers, Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
