Console Output

Skipping 304 KB.. Full Log

_Div ...
Processing theory List-Infinite.SetInterval2 ...
Processing theory List-Infinite.InfiniteSet2 ...
Processing theory List-Infinite.SetIntervalCut ...
Removing 3 theories ...
Processing theory List-Infinite.SetIntervalStep ...
Processing theory List-Infinite.List2 ...
Processing theory List-Infinite.ListInf ...
Processing theory AutoFocus-Stream.ListSlice ...
Processing theory List-Infinite.ListInf_Prefix ...
Processing theory Nat-Interval-Logic.IL_Interval ...
Processing theory AutoFocus-Stream.AF_Stream ...
Processing theory AutoFocus-Stream.AF_Stream_Exec ...
Processing theory Nat-Interval-Logic.IL_IntervalOperators ...
Processing theory Nat-Interval-Logic.IL_TemporalOperators ...
Processing theory AutoFocus-Stream.IL_AF_Stream ...
Processing theory AutoFocus-Stream.IL_AF_Stream_Exec ...
Loading 3 theories ...
Processing theory Architectural_Design_Patterns.Singleton ...
Processing theory Architectural_Design_Patterns.Publisher_Subscriber ...
Processing theory Architectural_Design_Patterns.Blackboard ...
Loading 12 theories ...
Processing theory Isabelle_Marries_Dirac.Basics ...
Processing theory Matrix.Ordered_Semiring ...
Removing 13 theories ...
Processing theory Isabelle_Marries_Dirac.Binary_Nat ...
Processing theory Matrix.Matrix_Legacy ...
Processing theory Isabelle_Marries_Dirac.Quantum ...
Processing theory Matrix_Tensor.Matrix_Tensor ...
Processing theory Isabelle_Marries_Dirac.Complex_Vectors ...
Processing theory Isabelle_Marries_Dirac.Tensor ...
Processing theory Isabelle_Marries_Dirac.Measurement ...
Processing theory Isabelle_Marries_Dirac.More_Tensor ...
Processing theory Isabelle_Marries_Dirac.Deutsch ...
Processing theory Isabelle_Marries_Dirac.Deutsch_Jozsa ...
Loading 170 theories ...
Processing theory CAVA_Base.Lexord_List ...
Processing theory CAVA_Base.Statistics ...
Processing theory Collections.Record_Intf ...
Processing theory Transition_Systems_and_Automata.Basic ...
Processing theory CAVA_Automata.Step_Conv ...
Removing 2 theories ...
Processing theory SM.SOS_Misc_Add ...
Processing theory SM.SM_Syntax ...
Processing theory Partial_Order_Reduction.Basic_Extensions ...
Processing theory Partial_Order_Reduction.Relation_Extensions ...
Processing theory Partial_Order_Reduction.Set_Extensions ...
Processing theory Partial_Order_Reduction.Functions ...
Processing theory Collections.Trie_Impl ...
Processing theory Transition_Systems_and_Automata.Sequence ...
Processing theory Transition_Systems_and_Automata.Transition_System ...
Processing theory Collections.Trie2 ...
Processing theory Collections.Dlist_add ...
Processing theory DFS_Framework.DFS_Framework_Misc ...
Processing theory Collections.Gen_Comp ...
Processing theory Partial_Order_Reduction.List_Extensions ...
Processing theory Partial_Order_Reduction.List_Prefixes ...
Processing theory CAVA_Automata.Digraph_Basic ...
Processing theory Partial_Order_Reduction.Word_Prefixes ...
Processing theory Collections.ICF_Spec_Base ...
Processing theory Collections.Sorted_List_Operations ...
Processing theory SM.SM_State ...
Processing theory Collections.DatRef ...
Processing theory Collections.ListSpec ...
Processing theory Collections.AnnotatedListSpec ...
Processing theory Partial_Order_Reduction.Traces ...
Processing theory Collections.FTAnnotatedListImpl ...
Processing theory Collections.ListGA ...
Processing theory Promela.PromelaAST ...
Processing theory LTL.LTL ...
Processing theory Stuttering_Equivalence.PLTL ...
Processing theory Collections.Fifo ...
Processing theory Collections.PrioSpec ...
Processing theory Collections.BinoPrioImpl ...
Processing theory Collections.SkewPrioImpl ...
Processing theory Collections.PrioByAnnotatedList ...
Processing theory Collections.PrioUniqueSpec ...
Processing theory Collections.MapSpec ...
Processing theory Collections.GenCF ...
Processing theory Collections.FTPrioImpl ...
Processing theory Collections.Refine_Dflt ...
Processing theory CAVA_Base.Code_String ...
Processing theory CAVA_Base.CAVA_Code_Target ...
Processing theory DFS_Framework.DFS_Framework_Refine_Aux ...
Processing theory Partial_Order_Reduction.ENat_Extensions ...
Processing theory Partial_Order_Reduction.CCPO_Extensions ...
Processing theory Collections.PrioUniqueByAnnotatedList ...
Processing theory Collections.FTPrioUniqueImpl ...
Processing theory Collections.SetSpec ...
Processing theory Collections.Algos ...
Processing theory Collections.SetIndex ...
Processing theory Collections.SetIteratorCollectionsGA ...
Processing theory Partial_Order_Reduction.ESet_Extensions ...
Processing theory Collections.MapGA ...
FAILED to process theory Collections.ArrayMapImpl
*** Error (line 360 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/ICF/impl/ArrayMapImpl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
FAILED to process theory Collections.ListMapImpl
*** Error (line 101 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/ICF/impl/ListMapImpl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Collections.SetGA ...
FAILED to process theory Collections.TrieMapImpl
*** Error (line 163 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/ICF/impl/TrieMapImpl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
FAILED to process theory Collections.ListSetImpl
*** Error (line 120 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/ICF/impl/ListSetImpl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
FAILED to process theory Collections.ListSetImpl_Invar
*** Error (line 105 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/ICF/impl/ListSetImpl_Invar.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Collections.ListMapImpl_Invar ...
Processing theory Collections.SetByMap ...
FAILED to process theory Collections.TrieSetImpl
*** Error (line 77 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/ICF/impl/TrieSetImpl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Partial_Order_Reduction.Coinductive_List_Extensions ...
Processing theory Partial_Order_Reduction.LList_Prefixes ...
Processing theory Collections.ArraySetImpl ...
FAILED to process theory Collections.ListSetImpl_NotDist
*** Error (line 202 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/ICF/impl/ListSetImpl_NotDist.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Collections.ArrayHashMap_Impl ...
FAILED to process theory Collections.ArrayHashMap
*** Error (line 168 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/ICF/impl/ArrayHashMap.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
FAILED to process theory Collections.ArrayHashSet
*** Error (line 77 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/ICF/impl/ArrayHashSet.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
FAILED to process theory Collections.RBTMapImpl
*** Error (line 135 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/ICF/impl/RBTMapImpl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Collections.ListSetImpl_Sorted ...
Processing theory Transition_Systems_and_Automata.Sequence_LTL ...
Processing theory Collections.HashMap_Impl ...
Processing theory Partial_Order_Reduction.Stuttering ...
Processing theory Transition_Systems_and_Automata.Transition_System_Construction ...
Processing theory Transition_Systems_and_Automata.Transition_System_Extra ...
FAILED to process theory Collections.HashMap
*** Error (line 201 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/ICF/impl/HashMap.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
FAILED to process theory Collections.RBTSetImpl
*** Error (line 102 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/ICF/impl/RBTSetImpl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Collections.MapStdImpl ...
Processing theory Partial_Order_Reduction.Transition_System_Extensions ...
Processing theory Partial_Order_Reduction.Transition_System_Traces ...
Processing theory Partial_Order_Reduction.Transition_System_Interpreted_Traces ...
Processing theory Collections.HashSet ...
Processing theory Collections.SetStdImpl ...
Processing theory Partial_Order_Reduction.Ample_Abstract ...
Processing theory Collections.ICF_Impl ...
Processing theory Collections.ICF_Refine_Monadic ...
Processing theory Partial_Order_Reduction.Ample_Analysis ...
Processing theory Collections.ICF_Autoref ...
Processing theory Collections.Collections ...
Processing theory Collections.CollectionsV1 ...
Processing theory CAVA_Base.CAVA_Base ...
Processing theory CAVA_Automata.Digraph ...
FAILED to process theory CAVA_LTL_Modelchecker.NDFS_SI_Statistics
*** Error (line 81 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_LTL_Modelchecker/Nested_DFS/NDFS_SI_Statistics.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Promela.PromelaStatistics ...
Processing theory LTL.Rewriting ...
Processing theory SM.LTS ...
Processing theory SM.SM_Cfg ...
Processing theory CAVA_Automata.Automata ...
Processing theory CAVA_Automata.Lasso ...
Processing theory CAVA_Automata.Simulation ...
Processing theory CAVA_Automata.Stuttering_Extension ...
FAILED to process theory CAVA_Automata.Digraph_Impl
*** Error (line 381 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_Automata/Digraph_Impl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory CAVA_LTL_Modelchecker.BoolProgs ...
Processing theory CAVA_LTL_Modelchecker.BoolProgs_Extras ...
Processing theory CAVA_LTL_Modelchecker.BoolProgs_LeaderFilters ...
Processing theory CAVA_LTL_Modelchecker.BoolProgs_Philosophers ...
Processing theory CAVA_LTL_Modelchecker.BoolProgs_ReaderWriter ...
Processing theory CAVA_LTL_Modelchecker.BoolProgs_Simple ...
Processing theory CAVA_LTL_Modelchecker.CAVA_Abstract ...
Processing theory CAVA_LTL_Modelchecker.BoolProgs_LTL_Conv ...
Processing theory SM.Gen_Scheduler ...
Processing theory Gabow_SCC.Find_Path ...
Processing theory SM.Gen_Scheduler_Refine ...
Processing theory SM.Gen_Cfg_Bisim ...
Processing theory SM.SM_Semantics ...
Processing theory SM.SM_LTL ...
Processing theory Gabow_SCC.Gabow_Skeleton ...
Processing theory SM.Decide_Locality ...
Processing theory SM.Type_System ...
Processing theory SM.SM_Finite_Reachable ...
FAILED to process theory Gabow_SCC.Find_Path_Impl
*** Error (line 345 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Gabow_SCC/Find_Path_Impl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory CAVA_Automata.Automata_Impl ...
FAILED to process theory SM.Rename_Cfg
*** Error (line 733 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_LTL_Modelchecker/SM/Refine/Rename_Cfg.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory SM.SM_Visible ...
FAILED to process theory Gabow_SCC.Gabow_Skeleton_Code
*** Error (line 269 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Gabow_SCC/Gabow_Skeleton_Code.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Gabow_SCC.Gabow_GBG ...
Processing theory CAVA_LTL_Modelchecker.BoolProgs_Programs ...
Processing theory DFS_Framework.Impl_Rev_Array_Stack ...
FAILED to process theory CAVA_LTL_Modelchecker.NDFS_SI
*** Error (line 1309 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_LTL_Modelchecker/Nested_DFS/NDFS_SI.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 1336 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_LTL_Modelchecker/Nested_DFS/NDFS_SI.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 1361 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_LTL_Modelchecker/Nested_DFS/NDFS_SI.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 1394 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_LTL_Modelchecker/Nested_DFS/NDFS_SI.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 1423 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_LTL_Modelchecker/Nested_DFS/NDFS_SI.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 1454 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_LTL_Modelchecker/Nested_DFS/NDFS_SI.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 1537 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_LTL_Modelchecker/Nested_DFS/NDFS_SI.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
FAILED to process theory Gabow_SCC.Gabow_GBG_Code
*** Error (line 320 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Gabow_SCC/Gabow_GBG_Code.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Promela.PromelaDatastructures ...
Processing theory Promela.PromelaInvariants ...
Processing theory DFS_Framework.Param_DFS ...
Processing theory DFS_Framework.General_DFS_Structure ...
Processing theory DFS_Framework.Tailrec_Impl ...
Processing theory DFS_Framework.Rec_Impl ...
Processing theory DFS_Framework.DFS_Invars_Basic ...
Processing theory SM.Pid_Scheduler ...
Processing theory SM.SM_Pid ...
Processing theory SM.SM_Variables ...
Processing theory DFS_Framework.Simple_Impl ...
Processing theory SM.SM_Indep ...
Processing theory DFS_Framework.Restr_Impl ...
Processing theory DFS_Framework.DFS_Framework ...
Processing theory Promela.Promela ...
Processing theory Promela.PromelaLTLConv ...
Processing theory Promela.PromelaLTL ...
FAILED to process theory DFS_Framework.Reachable_Nodes
*** Error (line 205 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/DFS_Framework/Examples/Reachable_Nodes.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 262 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/DFS_Framework/Examples/Reachable_Nodes.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
FAILED to process theory DFS_Framework.Feedback_Arcs
*** Error (line 388 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/DFS_Framework/Examples/Feedback_Arcs.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory SM.SM_Datastructures ...
Processing theory LTL_to_GBA.LTL_to_GBA ...
Processing theory SM.SM_Sticky ...
Processing theory SM.SM_POR ...
Processing theory LTL_to_GBA.LTL_to_GBA_impl ...
FAILED to process theory SM.SM_Ample_Impl
*** Error (line 494 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_LTL_Modelchecker/SM/Impl/SM_Ample_Impl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 527 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_LTL_Modelchecker/SM/Impl/SM_Ample_Impl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 1298 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_LTL_Modelchecker/SM/Impl/SM_Ample_Impl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory SM.SM_Wrapup ...
FAILED to process theory CAVA_LTL_Modelchecker.CAVA_Impl
*** Error (line 832 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_LTL_Modelchecker/CAVA_Impl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 1506 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_LTL_Modelchecker/CAVA_Impl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory CAVA_LTL_Modelchecker.Mulog ...
Loading 2 theories ...
Processing theory CAVA_LTL_Modelchecker.All_Of_Nested_DFS ...
Processing theory CAVA_LTL_Modelchecker.All_Of_CAVA_LTL_Modelchecker ...
Loading 3 theories ...
Removing 40 theories ...
Processing theory Polynomials.Poly_Mapping_Finite_Map ...
Processing theory Polynomials.MPoly_Type_Class_FMap ...
Processing theory Symmetric_Polynomials.Symmetric_Polynomials_Code ...
Processing theory Berlekamp_Zassenhaus.Hensel_Lifting_Type_Based ...
Removing 31 theories ...
Processing theory Isabelle_Marries_Dirac.Quantum_Teleportation ...
Removing 1 theories ...
Processing theory Isabelle_Marries_Dirac.Quantum_Prisoners_Dilemma ...
Processing theory Isabelle_Marries_Dirac.Entanglement ...
Loading 12 theories ...
Processing theory Transition_Systems_and_Automata.Sequence_Zip ...
Processing theory Adaptive_State_Counting.FSM ...
Removing 4 theories ...
Processing theory Adaptive_State_Counting.FSM_Product ...
Processing theory Adaptive_State_Counting.ATC ...
Processing theory Adaptive_State_Counting.ASC_LB ...
Processing theory Adaptive_State_Counting.ASC_Suite ...
Processing theory Adaptive_State_Counting.ASC_Sufficiency ...
Processing theory Adaptive_State_Counting.ASC_Hoare ...
Processing theory Adaptive_State_Counting.ASC_Example ...
Processing theory Dirichlet_Series.Dirichlet_Efficient_Code ...
Loading 18 theories ...
Processing theory Collections.Refine_Dflt_ICF ...
Processing theory Prpu_Maxflow.Graph_Topological_Ordering ...
Processing theory Flow_Networks.Fofu_Abs_Base ...
Processing theory Refine_Imperative_HOL.Sepref_ICF_Bindings ...
Removing 48 theories ...
Processing theory Flow_Networks.Fofu_Impl_Base ...
Processing theory Flow_Networks.Refine_Add_Fofu ...
Processing theory Flow_Networks.Graph_Impl ...
Processing theory Flow_Networks.Network_Impl ...
Processing theory Prpu_Maxflow.Generic_Push_Relabel ...
Processing theory Prpu_Maxflow.Prpu_Common_Inst ...
Processing theory Prpu_Maxflow.Fifo_Push_Relabel ...
Processing theory Prpu_Maxflow.Relabel_To_Front ...
FAILED to process theory Flow_Networks.NetCheck
*** Error (line 708 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Flow_Networks/NetCheck.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 1511 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Flow_Networks/NetCheck.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Prpu_Maxflow.Prpu_Common_Impl ...
FAILED to process theory Prpu_Maxflow.Relabel_To_Front_Impl
*** Error (line 413 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Prpu_Maxflow/Relabel_To_Front_Impl.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 494 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Prpu_Maxflow/Relabel_To_Front_Impl.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
FAILED to process theory Prpu_Maxflow.Fifo_Push_Relabel_Impl
*** Error (line 803 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Prpu_Maxflow/Fifo_Push_Relabel_Impl.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 893 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Prpu_Maxflow/Fifo_Push_Relabel_Impl.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 996 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Prpu_Maxflow/Fifo_Push_Relabel_Impl.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Prpu_Maxflow.Generated_Code_Test ...
Processing theory Isabelle_Marries_Dirac.No_Cloning ...
Loading 7 theories ...
Processing theory Saturation_Framework.Calculus ...
Processing theory Saturation_Framework.Calculus_Variations ...
Processing theory Saturation_Framework.Intersection_Calculus ...
Removing 36 theories ...
Processing theory Saturation_Framework.Lifting_to_Non_Ground_Calculi ...
Processing theory Saturation_Framework.Labeled_Lifting_to_Non_Ground_Calculi ...
Processing theory Saturation_Framework.Given_Clause_Architectures ...
Loading 4 theories ...
Processing theory Saturation_Framework_Extensions.Given_Clause_Architectures_Revisited ...
Processing theory Saturation_Framework_Extensions.Soundness ...
Processing theory Saturation_Framework_Extensions.Standard_Redundancy_Criterion ...
Processing theory Saturation_Framework_Extensions.Clausal_Calculus ...
Removing 1 theories ...
Processing theory Saturation_Framework_Extensions.FO_Ordered_Resolution_Prover_Revisited ...
Loading 3 theories ...
Removing 22 theories ...
Processing theory Stateful_Protocol_Composition_and_Typing.Example_TLS ...
Processing theory Stateful_Protocol_Composition_and_Typing.Example_Keyserver ...
Loading 6 theories ...
Processing theory Stateful_Protocol_Composition_and_Typing.Examples ...
Processing theory EdmondsKarp_Maxflow.FordFulkerson_Algo ...
Processing theory EdmondsKarp_Maxflow.EdmondsKarp_Algo ...
FAILED to process theory EdmondsKarp_Maxflow.Augmenting_Path_BFS
*** Error (line 731 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/EdmondsKarp_Maxflow/Augmenting_Path_BFS.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Removing 23 theories ...
FAILED to process theory EdmondsKarp_Maxflow.EdmondsKarp_Impl
*** Error (line 983 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/EdmondsKarp_Maxflow/EdmondsKarp_Impl.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
FAILED to process theory EdmondsKarp_Maxflow.Edka_Checked_Impl
*** Error (line 53 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/EdmondsKarp_Maxflow/Edka_Checked_Impl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory EdmondsKarp_Maxflow.Edka_Benchmark_Export ...
Loading 2 theories ...
Processing theory ShortestPath.ShortestPath ...
Loading 4 theories ...
Processing theory ShortestPath.ShortestPathNeg ...
Processing theory VerifyThis2019.Exc_Nres_Monad ...
Processing theory VerifyThis2019.VTcomp ...
FAILED to process theory VerifyThis2019.Challenge2A
*** Error (line 275 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/VerifyThis2019/Challenge2A.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory VerifyThis2019.Challenge2B ...
Loading 7 theories ...
Removing 45 theories ...
Processing theory VerifyThis2018.Synth_Definition ...
Processing theory VerifyThis2018.Dynamic_Array ...
Processing theory VerifyThis2018.DRAT_Misc ...
Processing theory VerifyThis2018.Array_Map_Default ...
Processing theory VerifyThis2018.Exc_Nres_Monad ...
Processing theory VerifyThis2018.VTcomp ...
FAILED to process theory VerifyThis2018.Snippets
*** Error (line 79 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/VerifyThis2018/Snippets.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 112 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/VerifyThis2018/Snippets.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 162 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/VerifyThis2018/Snippets.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Loading 2 theories ...
Processing theory VerifyThis2018.DF_System ...
Removing 1 theories ...
Processing theory VerifyThis2018.Challenge3 ...
Removing 2 theories ...
Processing theory VerifyThis2018.Challenge2 ...
Processing theory VerifyThis2018.Challenge1_short ...
Processing theory VerifyThis2018.Challenge1 ...
Loading 2 theories ...
Processing theory Partial_Order_Reduction.Formula ...
Processing theory Partial_Order_Reduction.Ample_Correctness ...
Loading 2 theories ...
Removing 32 theories ...
Processing theory CakeML.TypeSystem ...
Processing theory CakeML.TypeSystemAuxiliary ...
Processing theory CakeML.Code_Test_Haskell ...
Loading 23 theories ...
Removing 13 theories ...
Processing theory Dijkstra_Shortest_Path.Dijkstra_Misc ...
FAILED to process theory Collections_Examples.Succ_Graph
*** Error (line 74 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/Examples/Autoref/Succ_Graph.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 89 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/Examples/Autoref/Succ_Graph.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Refine_Imperative_HOL.Sepref_Snip_Combinator ...
Processing theory Refine_Imperative_HOL.Worklist_Subsumption ...
FAILED to process theory Refine_Imperative_HOL.Sepref_Graph
*** Error (line 79 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Refine_Imperative_HOL/Examples/Sepref_Graph.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Refine_Imperative_HOL.Worklist_Subsumption_Impl ...
FAILED to process theory Refine_Imperative_HOL.Sepref_DFS
*** Error (line 233 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Refine_Imperative_HOL/Examples/Sepref_DFS.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Refine_Imperative_HOL.Sepref_Snip_Datatype ...
Processing theory Dijkstra_Shortest_Path.GraphSpec ...
Processing theory Dijkstra_Shortest_Path.GraphGA ...
FAILED to process theory Refine_Imperative_HOL.Sepref_WGraph
*** Error (line 89 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Refine_Imperative_HOL/Examples/Sepref_WGraph.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Dijkstra_Shortest_Path.GraphByMap ...
Processing theory Dijkstra_Shortest_Path.Weight ...
FAILED to process theory Refine_Imperative_HOL.Sepref_Minitests
*** Error (line 309 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Refine_Imperative_HOL/Examples/Sepref_Minitests.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 334 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Refine_Imperative_HOL/Examples/Sepref_Minitests.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 344 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Refine_Imperative_HOL/Examples/Sepref_Minitests.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 395 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Refine_Imperative_HOL/Examples/Sepref_Minitests.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Dijkstra_Shortest_Path.HashGraphImpl ...
Processing theory Dijkstra_Shortest_Path.Dijkstra ...
FAILED to process theory Collections_Examples.Nested_DFS
*** Error (line 1100 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/Examples/Autoref/Nested_DFS.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
FAILED to process theory Refine_Imperative_HOL.Sepref_NDFS
*** Error (line 62 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Refine_Imperative_HOL/Examples/Sepref_NDFS.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 113 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Refine_Imperative_HOL/Examples/Sepref_NDFS.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 161 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Refine_Imperative_HOL/Examples/Sepref_NDFS.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
FAILED to process theory Dijkstra_Shortest_Path.Dijkstra_Impl_Adet
*** Error (line 392 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Dijkstra_Shortest_Path/Dijkstra_Impl_Adet.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 400 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Dijkstra_Shortest_Path/Dijkstra_Impl_Adet.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Dijkstra_Shortest_Path.Test ...
FAILED to process theory Refine_Imperative_HOL.Sepref_Dijkstra
*** Error (line 230 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Refine_Imperative_HOL/Examples/Sepref_Dijkstra.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Refine_Imperative_HOL.Sepref_All_Examples ...
Loading 45 theories ...
Processing theory Slicing.AuxLemmas ...
Processing theory Formal_SSA.Serial_Rel ...
Processing theory Slicing.BasicDefs ...
Processing theory Slicing.CFG ...
Processing theory Slicing.CFGExit ...
Processing theory Slicing.Postdomination ...
Processing theory Slicing.CFG_wf ...
Processing theory Slicing.CFGExit_wf ...
Processing theory Slicing.DynDataDependence ...
Processing theory Slicing.DataDependence ...
Processing theory Slicing.SemanticsCFG ...
Processing theory Slicing.Distance ...
Processing theory Slicing.Observable ...
Processing theory Slicing.WeakOrderDependence ...
Processing theory Slicing.Com ...
Removing 7 theories ...
Processing theory Slicing.DynWeakControlDependence ...
Processing theory Slicing.WeakControlDependence ...
Processing theory Slicing.DynStandardControlDependence ...
Processing theory Slicing.StandardControlDependence ...
Processing theory Slicing.Labels ...
Processing theory Formal_SSA.FormalSSA_Misc ...
Processing theory Formal_SSA.Mapping_Exts ...
Processing theory Formal_SSA.RBT_Mapping_Exts ...
Processing theory Formal_SSA.While_Combinator_Exts ...
Processing theory Slicing.PDG ...
Processing theory Slicing.WCFG ...
Processing theory Slicing.Interpretation ...
Processing theory Slicing.Slice ...
Processing theory Slicing.CDepInstantiations ...
Processing theory Slicing.WellFormed ...
Processing theory Formal_SSA.Graph_path ...
Processing theory Slicing.AdditionalLemmas ...
Processing theory Formal_SSA.Disjoin_Transform ...
Processing theory Formal_SSA.SSA_CFG ...
Processing theory Formal_SSA.Minimality ...
Processing theory Formal_SSA.SSA_CFG_code ...
Processing theory Formal_SSA.Construct_SSA ...
Processing theory Formal_SSA.Construct_SSA_notriv ...
Processing theory Formal_SSA.Construct_SSA_code ...
Processing theory Formal_SSA.SSA_Transfer_Rules ...
Processing theory Formal_SSA.Construct_SSA_notriv_code ...
Processing theory Formal_SSA.Generic_Interpretation ...
Processing theory Formal_SSA.WhileGraphSSA ...
Processing theory Formal_SSA.Generic_Extract ...
Processing theory Refine_Imperative_HOL.Dijkstra_Benchmark ...
Loading 2 theories ...
Removing 18 theories ...
Processing theory Refine_Imperative_HOL.NDFS_Benchmark ...
Loading 13 theories ...
Processing theory Kruskal.Kruskal_Misc ...
Processing theory Kruskal.UGraph ...
Processing theory Kruskal.MinWeightBasis ...
Processing theory Kruskal.Kruskal ...
Processing theory Kruskal.SeprefUF ...
Processing theory Kruskal.Kruskal_Refine ...
Removing 3 theories ...
Processing theory Kruskal.Kruskal_Impl ...
Processing theory Kruskal.UGraph_Impl ...
Loading 3 theories ...
Processing theory Kruskal.Graph_Definition ...
Processing theory Kruskal.Graph_Definition_Aux ...
Removing 2 theories ...
Processing theory Kruskal.Graph_Definition_Impl ...
Processing theory PAC_Checker.PAC_Assoc_Map_Rel ...
Processing theory Refine_Imperative_HOL.Heapmap_Bench ...
Processing theory CakeML.BigSmallInvariants ...
Loading 3 theories ...
Removing 20 theories ...
Processing theory Floyd_Warshall.Recursion_Combinators ...
Processing theory Floyd_Warshall.Floyd_Warshall ...
FAILED to process theory Floyd_Warshall.FW_Code
*** Error (line 106 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Floyd_Warshall/FW_Code.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Loading 4 theories ...
Removing 3 theories ...
Processing theory Special_Function_Bounds.Bounds_Lemmas ...
Processing theory Special_Function_Bounds.Exp_Bounds ...
Removing 1 theories ...
Processing theory Sturm_Sequences.Sturm_Ex ...
Loading 2 theories ...
Processing theory VerifyThis2019.Parallel_Multiset_Fold ...
Processing theory VerifyThis2019.Challenge3 ...
Processing theory Refine_Imperative_HOL.Sepref_Guide_Reference ...
Removing 12 theories ...
FAILED to process theory Refine_Imperative_HOL.Sepref_Guide_Quickstart
*** Error (line 132 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Refine_Imperative_HOL/Userguides/Sepref_Guide_Quickstart.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 271 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Refine_Imperative_HOL/Userguides/Sepref_Guide_Quickstart.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Refine_Imperative_HOL.Sepref_Guide_General_Util ...
Removing 2 theories ...
Processing theory Knuth_Morris_Pratt.KMP ...
Loading 2 theories ...
Processing theory Complex_Geometry.Riemann_Sphere ...
Removing 21 theories ...
Processing theory Complex_Geometry.Chordal_Metric ...
Loading 54 theories ...
Processing theory UTP-Toolkit.List_Lexord_Alt ...
Processing theory UTP-Toolkit.Total_Recall ...
Processing theory UTP.utp_parser_utils ...
Processing theory UTP-Toolkit.Infinity ...
Processing theory UTP-Toolkit.Positive ...
Processing theory UTP-Toolkit.FSet_Extra ...
Processing theory UTP-Toolkit.Map_Extra ...
Removing 23 theories ...
Processing theory UTP-Toolkit.Partial_Fun ...
Processing theory UTP-Toolkit.Finite_Fun ...
Processing theory UTP-Toolkit.List_Extra ...
Processing theory UTP-Toolkit.Sequence ...
Processing theory UTP-Toolkit.Countable_Set_Extra ...
Processing theory UTP-Toolkit.utp_toolkit ...
Processing theory UTP.utp_var ...
Processing theory UTP.utp_expr ...
Processing theory UTP.utp_expr_insts ...
Processing theory UTP.utp_expr_funcs ...
Processing theory UTP.utp_unrest ...
Processing theory UTP.utp_usedby ...
Processing theory UTP.utp_tactics ...
Processing theory UTP.utp_subst ...
Processing theory UTP.utp_meta_subst ...
Processing theory UTP.utp_pred ...
Processing theory UTP.utp_alphabet ...
Processing theory UTP.utp_lift ...
Processing theory UTP.utp_pred_laws ...
Processing theory UTP.utp_healthy ...
Processing theory UTP.utp_sequent ...
Processing theory UTP.utp_rel ...
Processing theory UTP.utp_recursion ...
Processing theory UTP.utp_state_parser ...
Processing theory UTP.utp_rel_laws ...
Processing theory UTP.utp_theory ...
Processing theory UTP.utp_hoare ...
Processing theory UTP.utp_rel_opsem ...
Processing theory UTP.utp_sym_eval ...
Processing theory UTP.utp_wp ...
Processing theory UTP.utp_dynlog ...
Processing theory UTP.utp_sp ...
Processing theory UTP.utp_concurrency ...
Processing theory UTP.utp ...
Processing theory UTP.utp_expr_ovld ...
Processing theory UTP.utp_full ...
Processing theory UTP.utp_easy_parser ...
Processing theory UTP.sum_list ...
Removing 4 theories ...
Processing theory CakeML.CakeML_Quickcheck ...
Loading 29 theories ...
Processing theory Buchi_Complementation.Alternate ...
Processing theory Transition_Systems_and_Automata.Acceptance ...
Processing theory Transition_Systems_and_Automata.Maps ...
Processing theory Transition_Systems_and_Automata.Refine ...
Processing theory Buchi_Complementation.Formula ...
Removing 5 theories ...
Processing theory Transition_Systems_and_Automata.Degeneralization ...
Processing theory Transition_Systems_and_Automata.Degeneralization_Refine ...
Processing theory Transition_Systems_and_Automata.Transition_System_Refine ...
Processing theory Transition_Systems_and_Automata.Implement ...
Processing theory Transition_Systems_and_Automata.Nondeterministic ...
Processing theory Transition_Systems_and_Automata.NBA ...
Processing theory Buchi_Complementation.Graph ...
Processing theory Transition_Systems_and_Automata.NGBA ...
Processing theory Transition_Systems_and_Automata.NBA_Combine ...
Processing theory Transition_Systems_and_Automata.NGBA_Refine ...
Processing theory Buchi_Complementation.Ranking ...
Processing theory Transition_Systems_and_Automata.NBA_Graphs ...
Processing theory Transition_Systems_and_Automata.NBA_Refine ...
Processing theory Transition_Systems_and_Automata.NGBA_Graphs ...
Processing theory Transition_Systems_and_Automata.NGBA_Implement ...
Processing theory Transition_Systems_and_Automata.NBA_Implement ...
Processing theory Buchi_Complementation.Complementation ...
Processing theory Transition_Systems_and_Automata.NBA_Algorithms ...
Processing theory Transition_Systems_and_Automata.NBA_Explicit ...
Processing theory Transition_Systems_and_Automata.NGBA_Algorithms ...
Processing theory Transition_Systems_and_Automata.NBA_Translate ...
Processing theory Buchi_Complementation.Complementation_Implement ...
Processing theory Buchi_Complementation.Complementation_Final ...
Processing theory Buchi_Complementation.Complementation_Build ...
Removing 22 theories ...
Processing theory LTL_to_GBA.All_Of_LTL_to_GBA ...
Processing theory UTP.utp_simple_time ...
Loading 12 theories ...
Processing theory Coinductive.Quotient_Coinductive_List ...
Processing theory Coinductive.Quotient_TLList ...
Loading 6 theories ...
Processing theory Coinductive.Coinductive ...
Processing theory Lazy-Lists-II.LList2 ...
Processing theory Topology.Topology ...
Processing theory Topology.LList_Topology ...
Removing 64 theories ...
Processing theory Chandy_Lamport.Util ...
Processing theory Chandy_Lamport.Distributed_System ...
Processing theory Chandy_Lamport.Trace ...
Processing theory Chandy_Lamport.Swap ...
Processing theory Chandy_Lamport.Snapshot ...
Loading 2 theories ...
Processing theory Chandy_Lamport.Co_Snapshot ...
Removing 3 theories ...
Processing theory Coinductive.Lazy_LList ...
Loading 7 theories ...
Processing theory Coinductive.Lazy_TLList ...
Processing theory DFS_Framework.DFS_Invars_SCC ...
Processing theory DFS_Framework.Tarjan_LowLink ...
Removing 3 theories ...
Processing theory DFS_Framework.Tarjan ...
FAILED to process theory DFS_Framework.Cyc_Check
*** Error (line 471 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/DFS_Framework/Examples/Cyc_Check.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
FAILED to process theory DFS_Framework.DFS_Find_Path
*** Error (line 648 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/DFS_Framework/Examples/DFS_Find_Path.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Loading 4 theories ...
FAILED to process theory DFS_Framework.Nested_DFS
*** Error (line 940 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/DFS_Framework/Examples/Nested_DFS.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory DFS_Framework.DFS_All_Examples ...
Processing theory Stream_Fusion_Code.Stream_Fusion ...
Removing 8 theories ...
Processing theory Stream_Fusion_Code.Stream_Fusion_List ...
Processing theory Stream_Fusion_Code.Stream_Fusion_LList ...
Loading 12 theories ...
Processing theory Stream_Fusion_Code.Stream_Fusion_Examples ...
Processing theory Knot_Theory.Tangle_Relation ...
Processing theory Knot_Theory.Preliminaries ...
Processing theory Knot_Theory.Tangles ...
Processing theory Knot_Theory.Tangle_Algebra ...
Processing theory Knot_Theory.Tangle_Moves ...
Processing theory Knot_Theory.Link_Algebra ...
Removing 4 theories ...
Processing theory Knot_Theory.Kauffman_Matrix ...
Processing theory Knot_Theory.Example ...
Processing theory Knot_Theory.Computations ...
Processing theory Knot_Theory.Linkrel_Kauffman ...
Loading 10 theories ...
Processing theory Knot_Theory.Kauffman_Invariance ...
Processing theory Knot_Theory.Knot_Theory ...
Removing 15 theories ...
Processing theory BTree.Basic_Assn ...
Processing theory BTree.Imperative_Loops ...
Processing theory BTree.BTree ...
Processing theory BTree.Array_SBlit ...
Processing theory BTree.Partially_Filled_Array ...
Processing theory BTree.BTree_Imp ...
Processing theory BTree.BTree_Set ...
Processing theory BTree.BTree_Split ...
Processing theory BTree.BTree_ImpSet ...
Processing theory BTree.BTree_ImpSplit ...
Processing theory Promela.All_Of_Promela ...
Removing 45 theories ...
Processing theory CakeML.SimpleIO ...
Loading 33 theories ...
Processing theory LTL_Master_Theorem.Quotient_Type ...
Processing theory LTL_Master_Theorem.Omega_Words_Fun_Stream ...
Processing theory Transition_Systems_and_Automata.Acceptance_Refine ...
Processing theory LTL.Equivalence_Relations ...
Processing theory LTL.Code_Equations ...
Processing theory LTL_Master_Theorem.Syntactic_Fragments_and_Stability ...
Processing theory Transition_Systems_and_Automata.Deterministic ...
Processing theory Transition_Systems_and_Automata.DBA ...
Processing theory Transition_Systems_and_Automata.DGBA ...
Processing theory Transition_Systems_and_Automata.DBA_Combine ...
Processing theory Transition_Systems_and_Automata.DCA ...
Processing theory LTL_Master_Theorem.After ...
Processing theory Transition_Systems_and_Automata.DGCA ...
Processing theory Transition_Systems_and_Automata.DCA_Combine ...
Processing theory Transition_Systems_and_Automata.DRA ...
Processing theory Transition_Systems_and_Automata.DRA_Combine ...
Processing theory Transition_Systems_and_Automata.DRA_Refine ...
Processing theory LTL.Disjunctive_Normal_Form ...
Processing theory Transition_Systems_and_Automata.DRA_Implement ...
Removing 2 theories ...
Processing theory Transition_Systems_and_Automata.DRA_Nodes ...
Processing theory LTL_Master_Theorem.Advice ...
Processing theory LTL_Master_Theorem.Transition_Functions ...
Processing theory LTL_Master_Theorem.Extra_Equivalence_Relations ...
Processing theory LTL_Master_Theorem.Master_Theorem ...
Processing theory Transition_Systems_and_Automata.DRA_Explicit ...
Processing theory LTL_Master_Theorem.Restricted_Master_Theorem ...
Processing theory Transition_Systems_and_Automata.DRA_Translate ...
Processing theory LTL_Master_Theorem.DRA_Construction ...
Processing theory LTL_Master_Theorem.DRA_Implementation ...
Processing theory LTL_Master_Theorem.DRA_Instantiation ...
Processing theory LTL_Master_Theorem.Code_Export ...
Loading 3 theories ...
Processing theory Gabow_SCC.Gabow_SCC ...
Removing 39 theories ...
Processing theory Gabow_SCC.Gabow_SCC_Code ...
Loading 19 theories ...
Processing theory Gabow_SCC.All_Of_Gabow_SCC ...
Processing theory HRB-Slicing.AuxLemmas ...
Processing theory HRB-Slicing.BasicDefs ...
Removing 9 theories ...
Processing theory HRB-Slicing.CFG ...
Processing theory HRB-Slicing.CFGExit ...
Processing theory HRB-Slicing.CFG_wf ...
Processing theory HRB-Slicing.CFGExit_wf ...
Processing theory HRB-Slicing.Distance ...
Processing theory HRB-Slicing.ReturnAndCallNodes ...
Processing theory HRB-Slicing.Observable ...
Processing theory HRB-Slicing.SemanticsCFG ...
Processing theory HRB-Slicing.Postdomination ...
Processing theory HRB-Slicing.SDG ...
Processing theory HRB-Slicing.HRBSlice ...
Processing theory HRB-Slicing.SCDObservable ...
Processing theory HRB-Slicing.Slice ...
Processing theory HRB-Slicing.WeakSimulation ...
Processing theory HRB-Slicing.FundamentalProperty ...
Processing theory InformationFlowSlicing_Inter.NonInterferenceInter ...
Processing theory InformationFlowSlicing_Inter.LiftingInter ...
Removing 2 theories ...
Processing theory CakeML.LibAuxiliary ...
Loading 6 theories ...
Processing theory Collections_Examples.Exploration ...
Processing theory Tree-Automata.Tree ...
Processing theory Tree-Automata.Ta ...
Removing 5 theories ...
Processing theory Tree-Automata.AbsAlgo ...
Processing theory Tree-Automata.Ta_impl ...
Processing theory Tree-Automata.Ta_impl_codegen ...
Processing theory Minimal_SSA.Irreducible ...
Processing theory List-Infinite.ListInfinite ...
Loading 18 theories ...
Removing 21 theories ...
Processing theory Nested_Multisets_Ordinals.Nested_Multiset ...
Processing theory Nested_Multisets_Ordinals.Hereditary_Multiset ...
Processing theory Nested_Multisets_Ordinals.Syntactic_Ordinal ...
Processing theory Nested_Multisets_Ordinals.Signed_Multiset ...
Processing theory Nested_Multisets_Ordinals.Signed_Hereditary_Multiset ...
Processing theory Nested_Multisets_Ordinals.Signed_Syntactic_Ordinal ...
Processing theory Polynomials.Polynomials ...
Processing theory Lambda_Free_KBOs.Lambda_Free_KBO_Util ...
Processing theory Lambda_Free_KBOs.Lambda_Free_KBO_App ...
Processing theory Lambda_Free_KBOs.Lambda_Free_KBO_Std ...
Processing theory Lambda_Free_KBOs.Lambda_Free_KBO_Basic ...
Processing theory Lambda_Free_KBOs.Lambda_Encoding_KBO ...
Processing theory Lambda_Free_KBOs.Lambda_Free_TKBO_Coefs ...
Processing theory Lambda_Free_KBOs.Lambda_Free_KBOs ...
Processing theory Formal_SSA.SSA_Semantics ...
Loading 55 theories ...
Processing theory Jinja.Auxiliary ...
Processing theory Jinja.Type ...
Processing theory Jinja.Decl ...
Processing theory Jinja.TypeRel ...
Processing theory Jinja.Value ...
Processing theory Jinja.Objects ...
Processing theory Jinja.Exceptions ...
Processing theory Jinja.Conform ...
Processing theory Jinja.SystemClasses ...
Processing theory Jinja.JVMState ...
Processing theory HRB-Slicing.Com ...
Processing theory HRB-Slicing.Labels ...
Processing theory HRB-Slicing.ProcState ...
Removing 20 theories ...
Processing theory Jinja.WellForm ...
Processing theory Jinja.SemiType ...
Processing theory Jinja.JVM_SemiType ...
Processing theory Jinja.JVMInstructions ...
Processing theory Jinja.JVMExceptions ...
Processing theory Jinja.JVMExecInstr ...
Processing theory Jinja.JVMExec ...
Processing theory Jinja.JVMListExample ...
Processing theory HRB-Slicing.PCFG ...
Processing theory HRB-Slicing.WellFormProgs ...
Processing theory Jinja.Effect ...
Processing theory Jinja.BVSpec ...
Processing theory Jinja.BVConform ...
Processing theory Jinja.EffectMono ...
Processing theory HRB-Slicing.Interpretation ...
Processing theory Jinja.TF_JVM ...
Processing theory Jinja.BVExec ...
Processing theory HRB-Slicing.WellFormed ...
Processing theory Jinja.BVSpecTypeSafe ...
Processing theory Jinja.BVExample ...
Processing theory HRB-Slicing.ValidPaths ...
Processing theory HRB-Slicing.ProcSDG ...
Processing theory HRB-Slicing.JVMCFG ...
Processing theory HRB-Slicing.JVMInterpretation ...
Processing theory HRB-Slicing.JVMPostdomination ...
Processing theory HRB-Slicing.JVMCFG_wf ...
Processing theory HRB-Slicing.JVMSDG ...
Loading 7 theories ...
Processing theory HRB-Slicing.HRBSlicing ...
Processing theory Core_DOM.Testing_Utils ...
Processing theory Core_DOM.Core_DOM_BaseTest ...
Processing theory Core_DOM.Document_adoptNode ...
Removing 32 theories ...
Processing theory Core_DOM.Document_getElementById ...
Processing theory Core_DOM.Node_insertBefore ...
Processing theory Core_DOM.Node_removeChild ...
Processing theory Core_DOM.Core_DOM_Tests ...
Processing theory CAVA_Automata.All_Of_CAVA_Automata ...
Loading 2 theories ...
Processing theory IEEE_Floating_Point.Conversion_IEEE_Float ...
Loading 17 theories ...
Processing theory IEEE_Floating_Point.Double ...
Removing 48 theories ...
Processing theory Word_Lib.Hex_Words ...
Processing theory Word_Lib.Legacy_Aliases ...
Processing theory Word_Lib.Word_16 ...
Processing theory Word_Lib.Norm_Words ...
Processing theory Word_Lib.Next_and_Prev ...
Processing theory Word_Lib.More_Sublist ...
Processing theory Word_Lib.Many_More ...
Processing theory Word_Lib.Word_8 ...
Processing theory Word_Lib.Ancient_Numeral ...
Processing theory Word_Lib.Bitwise ...
Processing theory Word_Lib.Bitwise_Signed ...
Processing theory Word_Lib.Word_32 ...
Processing theory Interval_Arithmetic_Word32.Finite_String ...
Processing theory Word_Lib.Strict_part_mono ...
Processing theory Word_Lib.Word_Lib_Sumo ...
Processing theory Interval_Arithmetic_Word32.Interval_Word32 ...
Processing theory Interval_Arithmetic_Word32.Interpreter ...
Loading 6 theories ...
Processing theory Jordan_Normal_Form.Derivation_Bound ...
Processing theory Jordan_Normal_Form.Show_Arctic ...
Processing theory Jordan_Normal_Form.Ring_Hom_Matrix ...
Processing theory Jordan_Normal_Form.Complexity_Carrier ...
Removing 11 theories ...
Processing theory Jordan_Normal_Form.Matrix_Comparison ...
Processing theory Jordan_Normal_Form.Matrix_Complexity ...
Loading 4 theories ...
Removing 7 theories ...
Processing theory MFOTL_Monitor.MFOTL ...
Processing theory MFOTL_Monitor.Monitor ...
Processing theory MFOTL_Monitor.Monitor_Code ...
Processing theory MFOTL_Monitor.Examples ...
Loading 2 theories ...
Removing 3 theories ...
Processing theory Jordan_Normal_Form.Strassen_Algorithm ...
Loading 4 theories ...
Processing theory Jordan_Normal_Form.Strassen_Algorithm_Code ...
Processing theory Transition_Systems_and_Automata.NFA ...
Processing theory Transition_Systems_and_Automata.NBTA ...
Loading 3 theories ...
Processing theory Transition_Systems_and_Automata.NGBTA ...
Processing theory Transition_Systems_and_Automata.NBTA_Combine ...
Removing 19 theories ...
Processing theory Containers.TwoSat_Ex ...
Processing theory Containers.Containers_DFS_Ex ...
FAILED to process theory Containers.Containers_TwoSat_Ex
*** Error (line 236 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Containers/Examples/Containers_TwoSat_Ex.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 250 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Containers/Examples/Containers_TwoSat_Ex.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 320 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Containers/Examples/Containers_TwoSat_Ex.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Loading 7 theories ...
Removing 2 theories ...
Processing theory Core_SC_DOM.Testing_Utils ...
Processing theory Core_SC_DOM.Core_DOM_BaseTest ...
Processing theory Core_SC_DOM.Document_adoptNode ...
Processing theory Core_SC_DOM.Node_insertBefore ...
Processing theory Core_SC_DOM.Node_removeChild ...
Processing theory Core_SC_DOM.Document_getElementById ...
Loading 3 theories ...
Processing theory Core_SC_DOM.Core_DOM_Tests ...
Removing 32 theories ...
Processing theory Transition_Systems_and_Automata.DBTA ...
Processing theory Transition_Systems_and_Automata.DGBTA ...
Processing theory Transition_Systems_and_Automata.DBTA_Combine ...
Processing theory CakeML.NamespaceAuxiliary ...
Processing theory Transition_Systems_and_Automata.DFA ...
Removing 16 theories ...
Processing theory CakeML.Tokens ...
Loading 21 theories ...
Processing theory Priority_Search_Trees.Prio_Map_Specs ...
Processing theory Priority_Search_Trees.PST_General ...
Processing theory Prim_Dijkstra_Simple.Common ...
Processing theory Prim_Dijkstra_Simple.Undirected_Graph ...
Processing theory Prim_Dijkstra_Simple.Undirected_Graph_Specs ...
Processing theory Priority_Search_Trees.PST_RBT ...
Removing 31 theories ...
Processing theory Prim_Dijkstra_Simple.Undirected_Graph_Impl ...
Processing theory Prim_Dijkstra_Simple.Prim_Abstract ...
FAILED to process theory Prim_Dijkstra_Simple.Prim_Impl
*** Error (line 451 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Prim_Dijkstra_Simple/Prim_Impl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Loading 17 theories ...
Processing theory Collections_Examples.Exploration_DFS ...
Processing theory Refine_Monadic.Breadth_First_Search ...
Removing 14 theories ...
Processing theory Collections.Refine_Dflt_Only_ICF ...
Processing theory Collections_Examples.ICF_Only_Test ...
FAILED to process theory Collections_Examples.PerformanceTest
*** Error (line 114 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/Examples/ICF/PerformanceTest.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
FAILED to process theory Collections_Examples.Simple_DFS
*** Error (line 297 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/Examples/Autoref/Simple_DFS.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 419 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/Examples/Autoref/Simple_DFS.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
FAILED to process theory Collections_Examples.Foreach_Refine
*** Error (line 122 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/Examples/Refine_Monadic/Foreach_Refine.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Collections_Examples.Refine_Fold ...
FAILED to process theory Collections_Examples.Combined_TwoSat
*** Error (line 171 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/Examples/Autoref/Combined_TwoSat.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 173 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/Examples/Autoref/Combined_TwoSat.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
FAILED to process theory Collections_Examples.itp_2010
*** Error (line 53 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/Examples/ICF/itp_2010.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Collections_Examples.ICF_Examples ...
FAILED to process theory Collections_Examples.Coll_Test
*** Error (line 462 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/Examples/Autoref/Coll_Test.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
FAILED to process theory Collections_Examples.Bfs_Impl
*** Error (line 174 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/Examples/Refine_Monadic/Bfs_Impl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Collections_Examples.Refine_Monadic_Examples ...
Processing theory Collections_Examples.ICF_Test ...
Processing theory Collections_Examples.Collection_Autoref_Examples ...
Loading 6 theories ...
Processing theory Collections_Examples.Collection_Examples ...
Processing theory Containers.Card_Datatype ...
Processing theory Containers.List_Proper_Interval ...
Processing theory Containers.Compatibility_Containers_Regular_Sets ...
FAILED to process theory Containers.Map_To_Mapping_Ex
*** Error (line 21 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Containers/Examples/Map_To_Mapping_Ex.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Containers-Benchmarks.Clauses ...
Removing 24 theories ...
Processing theory Containers.Containers_Userguide ...
Removing 7 theories ...
FAILED to process theory Dijkstra_Shortest_Path.Dijkstra_Impl
*** Error (line 231 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Dijkstra_Shortest_Path/Dijkstra_Impl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Loading 83 theories ...
Processing theory IP_Addresses.Hs_Compat ...
Processing theory Iptables_Semantics.List_Misc ...
Processing theory IP_Addresses.Lib_Numbers_toString ...
Processing theory Iptables_Semantics.Repeat_Stabilize ...
Processing theory IP_Addresses.Lib_List_toString ...
Processing theory Iptables_Semantics.Remdups_Rev ...
Processing theory Iptables_Semantics.Datatype_Selectors ...
Processing theory Routing.Linorder_Helper ...
Processing theory Simple_Firewall.Lib_Enum_toString ...
Processing theory Iptables_Semantics.Negation_Type ...
Processing theory Simple_Firewall.List_Product_More ...
FAILED to process theory Simple_Firewall.GroupF
*** Error (line 54 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Simple_Firewall/Common/GroupF.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Simple_Firewall.Firewall_Common_Decision_State ...
Processing theory IP_Addresses.NumberWang_IPv4 ...
Processing theory Simple_Firewall.IP_Partition_Preliminaries ...
Processing theory Iptables_Semantics.Conntrack_State ...
Processing theory Simple_Firewall.Iface ...
Processing theory Iptables_Semantics.Ternary ...
Processing theory Simple_Firewall.L4_Protocol ...
Processing theory Iptables_Semantics.L4_Protocol_Flags ...
Removing 10 theories ...
Processing theory Iptables_Semantics.Word_Upto ...
Processing theory Simple_Firewall.Simple_Packet ...
Processing theory Iptables_Semantics.Tagged_Packet ...
Processing theory Simple_Firewall.SimpleFw_Syntax ...
Processing theory IP_Addresses.NumberWang_IPv6 ...
Processing theory IP_Addresses.Lib_Word_toString ...
Processing theory Iptables_Semantics.Firewall_Common ...
Processing theory Iptables_Semantics.Matching_Ternary ...
Processing theory Iptables_Semantics.Unknown_Match_Tacs ...
Processing theory IP_Addresses.WordInterval ...
Processing theory IP_Addresses.WordInterval_Sorted ...
Processing theory Iptables_Semantics.WordInterval_Lists ...
Processing theory Iptables_Semantics.Ports ...
FAILED to process theory IP_Addresses.IP_Address
*** Error (line 401 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/IP_Addresses/IP_Address.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Iptables_Semantics.Semantics_Ternary ...
Processing theory Iptables_Semantics.Fixed_Action ...
Processing theory Iptables_Semantics.Normalized_Matches ...
Processing theory Iptables_Semantics.Negation_Type_Matching ...
Processing theory Iptables_Semantics.Optimizing ...
Processing theory Iptables_Semantics.Semantics ...
Processing theory IP_Addresses.IPv4 ...
Processing theory Iptables_Semantics.Matching ...
Processing theory Iptables_Semantics.Ruleset_Update ...
Processing theory IP_Addresses.Prefix_Match ...
Processing theory IP_Addresses.CIDR_Split ...
Processing theory Iptables_Semantics.Semantics_Goto ...
Processing theory Simple_Firewall.SimpleFw_Semantics ...
Processing theory Iptables_Semantics.Primitive_Normalization ...
Processing theory Iptables_Semantics.MatchExpr_Fold ...
Processing theory Iptables_Semantics.Call_Return_Unfolding ...
Processing theory IP_Addresses.IPv6 ...
Processing theory IP_Addresses.IP_Address_Parser ...
Processing theory IP_Addresses.IP_Address_toString ...
Processing theory IP_Addresses.Prefix_Match_toString ...
Processing theory Simple_Firewall.IP_Addr_WordInterval_toString ...
Processing theory Simple_Firewall.Primitives_toString ...
Processing theory Simple_Firewall.SimpleFw_toString ...
Processing theory Routing.Routing_Table ...
Processing theory Iptables_Semantics.IpAddresses ...
Processing theory Simple_Firewall.Service_Matrix ...
Processing theory Iptables_Semantics.Common_Primitive_Syntax ...
Processing theory Iptables_Semantics.Common_Primitive_Matcher_Generic ...
Processing theory Iptables_Semantics.Ipassmt ...
Processing theory Iptables_Semantics.Routing_IpAssmt ...
Processing theory Iptables_Semantics.Common_Primitive_Matcher ...
Processing theory Iptables_Semantics.Common_Primitive_Lemmas ...
Processing theory Iptables_Semantics.Interfaces_Normalize ...
Processing theory Iptables_Semantics.Conntrack_State_Transform ...
Processing theory Iptables_Semantics.Common_Primitive_toString ...
Processing theory Iptables_Semantics.Protocols_Normalize ...
Processing theory Iptables_Semantics.Output_Interface_Replace ...
Processing theory Iptables_Semantics.IpAddresses_Normalize ...
Processing theory Iptables_Semantics.Ports_Normalize ...
Processing theory Iptables_Semantics.No_Spoof ...
Processing theory Iptables_Semantics.Interface_Replace ...
Processing theory Iptables_Semantics.Transform ...
Processing theory Iptables_Semantics.Primitive_Abstract ...
Processing theory Iptables_Semantics.SimpleFw_Compliance ...
Processing theory Iptables_Semantics.Code_Interface ...
Processing theory Iptables_Semantics_Examples.iptables_Ln_tuned_parsed ...
Processing theory Iptables_Semantics.Parser ...
Processing theory Iptables_Semantics.Parser6 ...
Processing theory Iptables_Semantics_Examples.Analyze_Synology_Diskstation ...
Processing theory Iptables_Semantics_Examples.Parser6_Test ...
Loading 13 theories ...
Removing 4 theories ...
Processing theory Simple_Firewall.Option_Helpers ...
Processing theory LOFT.OpenFlow_Helpers ...
Processing theory LOFT.Sort_Descending ...
Processing theory LOFT.List_Group ...
Processing theory Simple_Firewall.Generic_SimpleFw ...
Processing theory Routing.Linux_Router ...
Processing theory LOFT.Semantics_OpenFlow ...
Processing theory Routing.IpRoute_Parser ...
Processing theory LOFT.OpenFlow_Matches ...
Processing theory LOFT.OpenFlow_Action ...
Processing theory LOFT.OpenFlow_Serialize ...
Processing theory LOFT.LinuxRouter_OpenFlow_Translation ...
Processing theory LOFT.RFC2544 ...
Removing 1 theories ...
Processing theory LOFT.OF_conv_test ...
Removing 2 theories ...
Processing theory Iptables_Semantics_Examples.SNS_IAS_Eduroam_Spoofing ...
Removing 1 theories ...
Processing theory Iptables_Semantics_Examples.Analyze_medium_sized_company ...
Removing 1 theories ...
Processing theory Iptables_Semantics_Examples.SQRL_2015_nospoof ...
Removing 1 theories ...
Processing theory Iptables_Semantics_Examples.Analyze_SQRL_Shorewall ...
Removing 1 theories ...
Processing theory Iptables_Semantics_Examples.Analyze_Ringofsaturn_com ...
Removing 1 theories ...
Processing theory Iptables_Semantics_Examples.Parser_Test ...
Removing 1 theories ...
Processing theory Iptables_Semantics_Examples.Contrived_Example ...
Processing theory Iptables_Semantics.Code_haskell ...
Loading 5 theories ...
Removing 4 theories ...
Processing theory Iptables_Semantics.Matching_Embeddings ...
Processing theory Iptables_Semantics.Semantics_Embeddings ...
Processing theory Iptables_Semantics.Access_Matrix_Embeddings ...
Processing theory Iptables_Semantics.No_Spoof_Embeddings ...
Processing theory Iptables_Semantics.Documentation ...
Loading 5 theories ...
Processing theory Containers-Benchmarks.Benchmark_Bool ...
Processing theory Containers-Benchmarks.Benchmark_Comparison ...
Processing theory Containers-Benchmarks.Benchmark_LC ...
Processing theory Containers-Benchmarks.Benchmark_Set ...
Processing theory Containers-Benchmarks.Benchmark_Set_LC ...
Processing theory CAVA_Base.All_Of_CAVA_Base ...
Removing 28 theories ...
Processing theory Containers-Benchmarks.Benchmark_ICF ...
Processing theory Iptables_Semantics.Iptables_Semantics ...
Loading 21 theories ...
Processing theory LTL_to_DRA.Map2 ...
Processing theory LTL_to_DRA.Preliminaries2 ...
Processing theory LTL_to_DRA.Mapping2 ...
Removing 5 theories ...
Processing theory LTL_to_DRA.List2 ...
Processing theory LTL_to_DRA.DTS ...
Processing theory LTL_to_DRA.Rabin ...
Processing theory LTL_to_DRA.LTL_FGXU ...
Processing theory LTL_to_DRA.LTL_Compat ...
Processing theory LTL_to_DRA.af ...
Processing theory LTL_to_DRA.LTL_Impl ...
Processing theory LTL_to_DRA.Logical_Characterization ...
Processing theory LTL_to_DRA.af_Impl ...
Processing theory LTL_to_DRA.Semi_Mojmir ...
Processing theory LTL_to_DRA.Mojmir ...
Processing theory LTL_to_DRA.Mojmir_Rabin ...
Processing theory LTL_to_DRA.Mojmir_Rabin_Impl ...
Processing theory LTL_to_DRA.LTL_Rabin ...
Processing theory LTL_to_DRA.LTL_Rabin_Unfold_Opt ...
Processing theory LTL_to_DRA.LTL_Rabin_Impl ...
Processing theory LTL_to_DRA.Export_Code ...
Loading 7 theories ...
Processing theory LTL.Example ...
Processing theory LTL_Normal_Form.Normal_Form ...
Processing theory Abstract_Soundness.Finite_Proof_Soundness ...
Processing theory LTL_Normal_Form.Normal_Form_Code_Export ...
Processing theory Abstract_Completeness.Propositional_Logic ...
Processing theory Abstract_Soundness.Infinite_Proof_Soundness ...
Removing 33 theories ...
Processing theory Iptables_Semantics_Examples.Small_Examples ...
Removing 1 theories ...
Processing theory Iptables_Semantics_Examples.Ports_Fail ...
Loading 13 theories ...
Processing theory Extended_Finite_State_Machines.FSet_Utils ...
Processing theory Extended_Finite_State_Machines.VName ...
Processing theory Extended_Finite_State_Machines.Trilean ...
Processing theory Extended_Finite_State_Machines.Value ...
Processing theory Extended_Finite_State_Machines.Value_Lexorder ...
Processing theory Extended_Finite_State_Machines.AExp ...
Removing 34 theories ...
Processing theory Extended_Finite_State_Machines.GExp ...
Processing theory Extended_Finite_State_Machines.Transition ...
Processing theory Extended_Finite_State_Machines.EFSM ...
Loading 11 theories ...
Processing theory Extended_Finite_State_Machines.Drinks_Machine ...
Processing theory Extended_Finite_State_Machines.EFSM_LTL ...
Processing theory Extended_Finite_State_Machines.Drinks_Machine_LTL ...
Removing 3 theories ...
FAILED to process theory CakeML_Codegen.Test_Utils
*** Error (line 65 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CakeML_Codegen/Utils/Test_Utils.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 67 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CakeML_Codegen/Utils/Test_Utils.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 75 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CakeML_Codegen/Utils/Test_Utils.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 83 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CakeML_Codegen/Utils/Test_Utils.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
FAILED to process theory Collections.Refine_Monadic_Userguide
*** Error (line 458 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/Userguides/Refine_Monadic_Userguide.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 530 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/Userguides/Refine_Monadic_Userguide.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Collections.ICF_Userguide ...
Loading 17 theories ...
Removing 59 theories ...
Processing theory Nested_Multisets_Ordinals.Goodstein_Sequence ...
Processing theory Prim_Dijkstra_Simple.Directed_Graph ...
Processing theory Ordinal.OrdinalDef ...
Processing theory Ordinal.OrdinalInduct ...
Processing theory Ordinal.OrdinalCont ...
Processing theory Ordinal.OrdinalRec ...
Processing theory Ordinal.OrdinalArith ...
Processing theory Ordinal.OrdinalInverse ...
Processing theory Ordinal.OrdinalFix ...
Processing theory Ordinal.OrdinalOmega ...
Processing theory Nested_Multisets_Ordinals.Syntactic_Ordinal_Bridge ...
Processing theory Prim_Dijkstra_Simple.Dijkstra_Abstract ...
Processing theory Prim_Dijkstra_Simple.Directed_Graph_Specs ...
Processing theory Prim_Dijkstra_Simple.Directed_Graph_Impl ...
Processing theory MFOTL_Monitor.Slicing ...
Processing theory Nested_Multisets_Ordinals.Hydra_Battle ...
FAILED to process theory Prim_Dijkstra_Simple.Dijkstra_Impl
*** Error (line 279 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Prim_Dijkstra_Simple/Dijkstra_Impl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Loading 2 theories ...
Processing theory Transitive-Closure.RBT_Map_Set_Extension ...
Loading 2 theories ...
Processing theory Transitive-Closure.Transitive_Closure_RBT_Impl ...
Processing theory Dynamic_Tables.Tables_real ...
Removing 40 theories ...
Processing theory Dynamic_Tables.Tables_nat ...
Processing theory DFS_Framework.On_Stack ...
Loading 28 theories ...
Processing theory Amortized_Complexity.Lemmas_log ...
Processing theory Amortized_Complexity.Priority_Queue_ops ...
Processing theory Amortized_Complexity.Priority_Queue_ops_merge ...
Processing theory Amortized_Complexity.Amortized_Framework ...
Processing theory Amortized_Complexity.Pairing_Heap_Tree_Analysis2 ...
Processing theory Amortized_Complexity.Pairing_Heap_List2_Analysis ...
Processing theory Amortized_Complexity.Pairing_Heap_List1_Analysis ...
Processing theory Amortized_Complexity.Pairing_Heap_Tree_Analysis ...
Processing theory Amortized_Complexity.Pairing_Heap_List1_Analysis2 ...
Removing 35 theories ...
Processing theory Amortized_Complexity.Amortized_Examples ...
Processing theory Cauchy.CauchySchwarz ...
Processing theory IMO2019.IMO2019_Q5 ...
Processing theory Special_Function_Bounds.Sin_Cos_Bounds ...
Processing theory Amortized_Complexity.Splay_Heap_Analysis ...
Processing theory Amortized_Complexity.Splay_Tree_Analysis_Base ...
Processing theory Amortized_Complexity.Skew_Heap_Analysis ...
Processing theory Special_Function_Bounds.Sqrt_Bounds ...
Processing theory Special_Function_Bounds.Log_CF_Bounds ...
Processing theory Amortized_Complexity.Splay_Tree_Analysis ...
Processing theory Amortized_Complexity.Splay_Tree_Analysis_Optimal ...
Processing theory Special_Function_Bounds.Atan_CF_Bounds ...
Removing 24 theories ...
Processing theory CakeML_Codegen.Test_Embed_Data ...
Loading 10 theories ...
Removing 18 theories ...
Processing theory Simpl.Simpl_Heap ...
Processing theory Simpl.HeapList ...
Processing theory BDD.BinDag ...
Processing theory BDD.General ...
Processing theory BDD.ProcedureSpecs ...
Processing theory BDD.RepointProof ...
Processing theory BDD.ShareRepProof ...
Processing theory BDD.LevellistProof ...
Processing theory BDD.ShareReduceRepListProof ...
Processing theory BDD.NormalizeTotalProof ...
Removing 5 theories ...
Processing theory Collections.Robdd ...
Loading 33 theories ...
Processing theory Syntax_Independent_Logic.Prelim ...
Processing theory HereditarilyFinite.Rank ...
Processing theory Nominal2.Nominal2_Base ...
Processing theory Nominal2.Nominal2_Abs ...
Removing 11 theories ...
Processing theory HereditarilyFinite.OrdArith ...
Processing theory Nominal2.Nominal2_FCB ...
Processing theory Nominal2.Nominal2 ...
Processing theory Goedel_HFSet_Semanticless.SyntaxN ...
Processing theory Goedel_HFSet_Semanticless.Coding ...
Processing theory Goedel_HFSet_Semanticless.Predicates ...
Processing theory Goedel_HFSet_Semanticless.Sigma ...
Processing theory Syntax_Independent_Logic.Syntax ...
Processing theory Goedel_HFSet_Semanticless.Coding_Predicates ...
Processing theory Goedel_HFSet_Semanticless.Pf_Predicates ...
Processing theory Syntax_Independent_Logic.Deduction ...
Processing theory Goedel_Incompleteness.Deduction2 ...
Processing theory Goedel_Incompleteness.Abstract_Encoding ...
Processing theory Syntax_Independent_Logic.Standard_Model ...
Processing theory Goedel_Incompleteness.Abstract_Representability ...
Processing theory Goedel_Incompleteness.Derivability_Conditions ...
Processing theory Goedel_Incompleteness.Diagonalization ...
Processing theory Goedel_Incompleteness.Goedel_Formula ...
Processing theory Goedel_Incompleteness.Standard_Model_More ...
Processing theory Goedel_Incompleteness.Abstract_First_Goedel ...
Processing theory Goedel_Incompleteness.Abstract_Second_Goedel ...
Processing theory Goedel_HFSet_Semanticless.Functions ...
Processing theory Goedel_HFSet_Semanticless.II_Prelims ...
Processing theory Goedel_HFSet_Semanticless.Pseudo_Coding ...
Processing theory Goedel_HFSet_Semanticless.Goedel_I ...
Processing theory Goedel_HFSet_Semanticless.Quote ...
Loading 13 theories ...
Processing theory Goedel_HFSet_Semanticless.Instance ...
Removing 12 theories ...
Processing theory Incompleteness.SyntaxN ...
Processing theory Incompleteness.Coding ...
Processing theory Incompleteness.Predicates ...
Processing theory Incompleteness.Sigma ...
Processing theory Incompleteness.Coding_Predicates ...
Processing theory Incompleteness.Pf_Predicates ...
Processing theory Incompleteness.Functions ...
Processing theory Incompleteness.Goedel_I ...
Processing theory Incompleteness.II_Prelims ...
Processing theory Incompleteness.Pseudo_Coding ...
Processing theory Incompleteness.Quote ...
Processing theory Incompleteness.Goedel_II ...
Removing 1 theories ...
Processing theory Goedel_HFSet_Semantic.Instance ...
Loading 3 theories ...
Processing theory Refine_Monadic.Example_Chapter ...
Loading 17 theories ...
Processing theory Refine_Monadic.WordRefine ...
Processing theory Refine_Monadic.Examples ...
Processing theory Simpl.Closure ...
Processing theory Simpl.XVcg ...
Processing theory Simpl.ProcParEx ...
Processing theory Simpl.Compose ...
Processing theory Simpl.SyntaxTest ...
Processing theory Simpl.XVcgEx ...
Processing theory Simpl.ClosureEx ...
Processing theory Simpl.ProcParExSP ...
Processing theory Simpl.ComposeEx ...
Processing theory Simpl.Quicksort ...
Processing theory Simpl.VcgExTotal ...
Removing 41 theories ...
Processing theory Simpl.AlternativeSmallStep ...
Processing theory Simpl.VcgEx ...
Processing theory Simpl.VcgExSP ...
Processing theory Simpl.UserGuide ...
Processing theory Simpl.Simpl ...
Processing theory Surprise_Paradox.Surprise_Paradox ...
Loading 2 theories ...
Processing theory LOFT.Featherweight_OpenFlow_Comparison ...
Processing theory LOFT.OpenFlow_Documentation ...
Removing 47 theories ...
Processing theory BDD.EvalProof ...
Loading 2 theories ...
Processing theory Simple_Firewall.Shadowed ...
Loading 13 theories ...
Processing theory Iptables_Semantics.Example_Semantics ...
Processing theory ROBDD.Option_Helpers ...
Processing theory ROBDD.Array_List ...
Processing theory ROBDD.Bool_Func ...
Processing theory ROBDD.Pointer_Map ...
Processing theory ROBDD.Pointer_Map_Impl ...
Processing theory Word_Lib.Guide ...
Processing theory ROBDD.BDT ...
Removing 74 theories ...
Processing theory ROBDD.Abstract_Impl ...
Processing theory ROBDD.Middle_Impl ...
Processing theory ROBDD.Conc_Impl ...
Loading 31 theories ...
Processing theory ROBDD.Level_Collapse ...
Processing theory ROBDD.BDD_Code ...
Processing theory ROBDD.BDD_Examples ...
Processing theory Complx.Cache_Tactics ...
Processing theory Word_Lib.Examples ...
Processing theory Native_Word.Uint16 ...
Processing theory Native_Word.Native_Cast ...
Processing theory Native_Word.Native_Cast_Uint ...
Processing theory Complx.Language ...
Removing 49 theories ...
Processing theory Complx.SmallStep ...
Processing theory Complx.OG_Annotations ...
Processing theory Complx.OG_Hoare ...
Processing theory Complx.SeqCatch_decomp ...
Processing theory Complx.OG_Soundness ...
Processing theory Complx.OG_Tactics ...
Processing theory Complx.OG_Syntax ...
Processing theory Complx.SumArr ...
Removing 17 theories ...
FAILED to process theory Native_Word.Native_Word_Test
*** Error (line 68 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Native_Word/Native_Word_Test.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 221 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Native_Word/Native_Word_Test.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 319 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Native_Word/Native_Word_Test.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 410 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Native_Word/Native_Word_Test.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 445 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Native_Word/Native_Word_Test.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Native_Word.Native_Word_Test_OCaml ...
FAILED to process theory Native_Word.Native_Word_Test_Emu
*** Error (line 22 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Native_Word/Native_Word_Test_Emu.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 52 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Native_Word/Native_Word_Test_Emu.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Native_Word.Native_Word_Test_MLton2 ...
Processing theory Native_Word.Native_Word_Test_PolyML2 ...
Processing theory Native_Word.Native_Word_Test_OCaml2 ...
Processing theory Native_Word.Native_Word_Test_PolyML64 ...
Processing theory Native_Word.Native_Word_Test_SMLNJ2 ...
Processing theory Native_Word.Native_Word_Test_PolyML ...
Processing theory Native_Word.Native_Word_Test_MLton ...
Processing theory Native_Word.Native_Word_Test_Scala ...
Removing 10 theories ...
Processing theory Native_Word.Native_Word_Test_GHC ...
Loading 47 theories ...
Processing theory Native_Word.Native_Word_Test_SMLNJ ...
Processing theory Deriving.Compare_Order_Instances ...
Processing theory Modal_Logics_for_NTS.FS_Set ...
Processing theory Datatype_Order_Generator.Hash_Generator ...
Processing theory Datatype_Order_Generator.Derive ...
Processing theory Old_Datatype_Show.Old_Show ...
Processing theory Old_Datatype_Show.Old_Show_Generator ...
Processing theory Old_Datatype_Show.Old_Show_Instances ...
Processing theory Modal_Logics_for_NTS.Residual ...
Processing theory Modal_Logics_for_NTS.Nominal_Wellfounded ...
Processing theory Modal_Logics_for_NTS.Transition_System ...
Removing 9 theories ...
Processing theory Modal_Logics_for_NTS.Weak_Transition_System ...
Processing theory Modal_Logics_for_NTS.Nominal_Bounded_Set ...
Processing theory Deriving.Derive_Examples ...
Processing theory Native_Word.Uint_Userguide ...
Processing theory Modal_Logics_for_NTS.FL_Transition_System ...
Removing 9 theories ...
Processing theory Modal_Logics_for_NTS.Formula ...
Processing theory Modal_Logics_for_NTS.Validity ...
Processing theory Modal_Logics_for_NTS.Disjunction ...
Processing theory Modal_Logics_for_NTS.Logical_Equivalence ...
Processing theory Modal_Logics_for_NTS.Bisimilarity_Implies_Equivalence ...
Processing theory Modal_Logics_for_NTS.Equivalence_Implies_Bisimilarity ...
Processing theory Modal_Logics_for_NTS.Weak_Formula ...
Processing theory Modal_Logics_for_NTS.Weak_Validity ...
Processing theory Modal_Logics_for_NTS.Weak_Logical_Equivalence ...
Processing theory Modal_Logics_for_NTS.Weak_Bisimilarity_Implies_Equivalence ...
Processing theory Modal_Logics_for_NTS.Weak_Equivalence_Implies_Bisimilarity ...
Processing theory Modal_Logics_for_NTS.Weak_Expressive_Completeness ...
Processing theory Modal_Logics_for_NTS.FL_Formula ...
Processing theory Modal_Logics_for_NTS.FL_Validity ...
Processing theory Modal_Logics_for_NTS.FL_Logical_Equivalence ...
Processing theory Modal_Logics_for_NTS.FL_Equivalence_Implies_Bisimilarity ...
Processing theory Modal_Logics_for_NTS.S_Transform ...
Processing theory Modal_Logics_for_NTS.FL_Bisimilarity_Implies_Equivalence ...
Processing theory Modal_Logics_for_NTS.L_Transform ...
Removing 16 theories ...
Processing theory Datatype_Order_Generator.Derive_Examples ...
Loading 100 theories ...
Processing theory Old_Datatype_Show.Old_Show_Examples ...
Processing theory Call_Arity.ConstOn ...
Processing theory Launchbury.Pointwise ...
Processing theory Launchbury.AList-Utils ...
Processing theory Launchbury.Vars ...
Processing theory Call_Arity.List-Interleavings ...
Removing 10 theories ...
Processing theory Launchbury.Nominal-Utils ...
Processing theory Launchbury.AList-Utils-Nominal ...
Processing theory Call_Arity.Set-Cpo ...
Processing theory Launchbury.HOLCF-Join ...
Processing theory Launchbury.HOLCF-Join-Classes ...
Processing theory Launchbury.HOLCF-Utils ...
Processing theory Call_Arity.Cardinality-Domain ...
Processing theory Launchbury.Terms ...
Processing theory Call_Arity.AList-Utils-HOLCF ...
Processing theory Call_Arity.Arity ...
Processing theory Launchbury.Env ...
Processing theory Call_Arity.Env-Set-Cpo ...
Processing theory Launchbury.Env-HOLCF ...
Processing theory Call_Arity.AEnv ...
Processing theory Launchbury.Nominal-HOLCF ...
Processing theory Call_Arity.Arity-Nominal ...
Processing theory Call_Arity.Cardinality-Domain-Lists ...
Processing theory Call_Arity.AnalBinds ...
Processing theory Call_Arity.TTree ...
Processing theory Call_Arity.TTree-HOLCF ...
Processing theory Call_Arity.CoCallGraph ...
Processing theory Call_Arity.CoCallGraph-Nominal ...
Processing theory Call_Arity.TTreeAnalysisSig ...
Processing theory Call_Arity.CoCallAnalysisSig ...
Processing theory Call_Arity.CoCallAnalysisBinds ...
Processing theory Launchbury.Substitution ...
Processing theory Call_Arity.ArityAnalysisSig ...
Processing theory Launchbury.Env-Nominal ...
Processing theory Call_Arity.CoCallAritySig ...
Processing theory Call_Arity.ArityAnalysisAbinds ...
Processing theory Call_Arity.ArityAnalysisFix ...
Processing theory Call_Arity.EtaExpansion ...
Processing theory Call_Arity.CoCallGraph-TTree ...
Processing theory Call_Arity.CoCallImplTTree ...
Processing theory Call_Arity.ArityAnalysisSpec ...
Processing theory Call_Arity.ArityAnalysisFixProps ...
Processing theory Call_Arity.CoCallAnalysisSpec ...
Processing theory Call_Arity.TTreeAnalysisSpec ...
Processing theory Call_Arity.CoCallImplTTreeSafe ...
Processing theory Call_Arity.CoCallFix ...
Processing theory Call_Arity.SestoftConf ...
Processing theory Call_Arity.ArityAnalysisStack ...
Processing theory Call_Arity.ArityStack ...
Processing theory Call_Arity.ArityConsistent ...
Processing theory Call_Arity.CardinalityAnalysisSig ...
Processing theory Call_Arity.CardinalityAnalysisSpec ...
Processing theory Call_Arity.TTreeImplCardinality ...
Processing theory Call_Arity.Sestoft ...
Processing theory Call_Arity.EtaExpansionSafe ...
Processing theory Call_Arity.TTreeImplCardinalitySafe ...
Processing theory Call_Arity.SestoftGC ...
Processing theory Call_Arity.TransformTools ...
Processing theory Call_Arity.ArityEtaExpansion ...
Processing theory Call_Arity.ArityEtaExpansionSafe ...
Processing theory Call_Arity.CoCallAnalysisImpl ...
Processing theory Call_Arity.CoCallImplSafe ...
Processing theory Call_Arity.AbstractTransform ...
Processing theory Call_Arity.ArityTransform ...
Processing theory Call_Arity.CallArityEnd2End ...
Processing theory Call_Arity.CardArityTransformSafe ...
Processing theory Call_Arity.CallArityEnd2EndSafe ...
Loading 15 theories ...
Processing theory Modal_Logics_for_NTS.Expressive_Completeness ...
Processing theory Aggregation_Algebras.Semigroups_Big ...
Removing 52 theories ...
Processing theory Stone_Algebras.Lattice_Basics ...
Processing theory Stone_Relation_Algebras.Fixpoints ...
Processing theory Stone_Relation_Algebras.Semirings ...
Processing theory Stone_Algebras.P_Algebras ...
Processing theory Stone_Kleene_Relation_Algebras.Iterings ...
Processing theory Stone_Kleene_Relation_Algebras.Kleene_Algebras ...
Processing theory Stone_Relation_Algebras.Relation_Algebras ...
Processing theory Stone_Relation_Algebras.Matrix_Relation_Algebras ...
Processing theory Stone_Kleene_Relation_Algebras.Kleene_Relation_Algebras ...
Processing theory Aggregation_Algebras.Aggregation_Algebras ...
Processing theory Stone_Kleene_Relation_Algebras.Matrix_Kleene_Algebras ...
Processing theory Aggregation_Algebras.Matrix_Aggregation_Algebras ...
Processing theory Aggregation_Algebras.Linear_Aggregation_Algebras ...
Loading 27 theories ...
Removing 4 theories ...
Processing theory Launchbury.Mono-Nat-Fun ...
Processing theory Launchbury.C ...
Processing theory Launchbury.Iterative ...
Processing theory Launchbury.CValue ...
Processing theory Launchbury.CValue-Nominal ...
Processing theory Launchbury.HasESem ...
Processing theory Launchbury.HOLCF-Meet ...
Processing theory Launchbury.C-Meet ...
Processing theory Launchbury.C-restr ...
Processing theory Launchbury.Value ...
Processing theory Launchbury.ValueSimilarity ...
Processing theory Launchbury.EvalHeap ...
Processing theory Launchbury.Value-Nominal ...
Processing theory Native_Word.Native_Word_Imperative_HOL ...
Processing theory Launchbury.HeapSemantics ...
Processing theory Launchbury.Launchbury ...
Processing theory Launchbury.AbstractDenotational ...
Processing theory Launchbury.Abstract-Denotational-Props ...
Processing theory Launchbury.Denotational ...
Processing theory Launchbury.CorrectnessOriginal ...
FAILED to process theory Collections.Locale_Code_Ex
*** Error (line 88 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/ICF/tools/Locale_Code_Ex.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Launchbury.ResourcedDenotational ...
Processing theory Launchbury.Denotational-Related ...
Processing theory Launchbury.CorrectnessResourced ...
Processing theory Launchbury.ResourcedAdequacy ...
Loading 9 theories ...
Processing theory Launchbury.Adequacy ...
Processing theory Launchbury.EverythingAdequacy ...
Processing theory LambdaAuth.Nominal2_Lemmas ...
Processing theory LambdaAuth.FMap_Lemmas ...
Removing 38 theories ...
Processing theory Relational_Minimum_Spanning_Trees.Kruskal ...
Processing theory LambdaAuth.Syntax ...
Processing theory LambdaAuth.Semantics ...
Processing theory LambdaAuth.Agreement ...
Processing theory LambdaAuth.Results ...
Processing theory Relational_Disjoint_Set_Forests.Disjoint_Set_Forests ...
Removing 6 theories ...
Processing theory Relational_Minimum_Spanning_Trees.Boruvka ...
Loading 56 theories ...
Processing theory Call_Arity.BalancedTraces ...
Processing theory UPF.Monads ...
Processing theory UPF_Firewall.Ports ...
Processing theory UPF_Firewall.NetworkCore ...
Processing theory UPF_Firewall.DatatypeAddress ...
Processing theory UPF_Firewall.DatatypePort ...
Processing theory UPF_Firewall.IPv4 ...
Processing theory UPF_Firewall.IPv4_TCPUDP ...
Processing theory UPF_Firewall.IntegerAddress ...
Processing theory UPF_Firewall.IntegerPort ...
Processing theory UPF_Firewall.IntegerPort_TCPUDP ...
Processing theory UPF_Firewall.NetworkModels ...
Processing theory Call_Arity.ArityAnalysisCorrDenotational ...
Processing theory UPF.UPFCore ...
Processing theory UPF.ElementaryPolicies ...
Processing theory UPF.ParallelComposition ...
Processing theory UPF.SeqComposition ...
Processing theory UPF_Firewall.LTL_alike ...
Processing theory Call_Arity.ArityTransformSafe ...
Processing theory Call_Arity.SestoftCorrect ...
Processing theory UPF.Analysis ...
Removing 28 theories ...
Processing theory UPF.Normalisation ...
Processing theory UPF.NormalisationTestSpecification ...
Processing theory UPF.UPF ...
Processing theory UPF_Firewall.PolicyCore ...
Processing theory UPF_Firewall.PolicyCombinators ...
Processing theory UPF_Firewall.PortCombinators ...
Processing theory UPF_Firewall.ProtocolPortCombinators ...
Processing theory UPF_Firewall.PacketFilter ...
Processing theory UPF_Firewall.NAT ...
Processing theory UPF_Firewall.StatefulCore ...
Processing theory UPF_Firewall.FTP ...
Processing theory UPF_Firewall.FTP_WithPolicy ...
Processing theory UPF_Firewall.VOIP ...
Processing theory UPF_Firewall.FWNormalisationCore ...
Processing theory UPF_Firewall.ElementaryRules ...
Processing theory UPF_Firewall.FTPVOIP ...
Processing theory UPF_Firewall.StatefulFW ...
Processing theory UPF_Firewall.NormalisationGenericProofs ...
Processing theory UPF_Firewall.NormalisationIntegerPortProof ...
Processing theory UPF_Firewall.NormalisationIPPProofs ...
Loading 8 theories ...
Processing theory UPF_Firewall.FWNormalisation ...
Processing theory UPF_Firewall.UPF-Firewall ...
Processing theory UPF_Firewall.DMZDatatype ...
Processing theory UPF_Firewall.DMZInteger ...
Processing theory UPF_Firewall.DMZ ...
Processing theory UPF_Firewall.PersonalFirewallDatatype ...
Processing theory UPF_Firewall.PersonalFirewallInt ...
Processing theory UPF_Firewall.PersonalFirewallIpv4 ...
Processing theory UPF_Firewall.PersonalFirewall ...
Processing theory UPF_Firewall.Transformation01 ...
Processing theory UPF_Firewall.Transformation02 ...
Processing theory UPF_Firewall.Transformation ...
Processing theory UPF_Firewall.Voice_over_IP ...
Processing theory UPF_Firewall.NAT-FW ...
Removing 43 theories ...
Processing theory UPF_Firewall.Examples ...
Processing theory Call_Arity.TrivialArityAnal ...
Processing theory Call_Arity.NoCardinalityAnalysis ...
Processing theory Chandy_Lamport.Example ...
Processing theory Syntax_Independent_Logic.Natural_Deduction ...
Processing theory Robinson_Arithmetic.Robinson_Arithmetic ...
Removing 34 theories ...
Processing theory Syntax_Independent_Logic.Syntax_Arith ...
Processing theory Syntax_Independent_Logic.Deduction_Q ...
Loading 32 theories ...
Processing theory Robinson_Arithmetic.Instance ...
Processing theory HOLCF-Prelude.HOLCF_Main ...
Processing theory HOLCF-Prelude.Data_Function ...
Processing theory HOLCF-Prelude.Numeral_Cpo ...
Processing theory HOLCF-Prelude.Type_Classes ...
Processing theory HOLCF-Prelude.Data_Bool ...
Processing theory Dependent_SIFUM_Type_Systems.Preliminaries ...
Processing theory HOLCF-Prelude.Data_Integer ...
Processing theory HOLCF-Prelude.Data_Tuple ...
Processing theory Dependent_SIFUM_Type_Systems.Security ...
Processing theory Dependent_SIFUM_Type_Systems.Language ...
Processing theory Dependent_SIFUM_Refinement.Eg2 ...
Removing 4 theories ...
Processing theory Dependent_SIFUM_Type_Systems.Compositionality ...
Processing theory HOLCF-Prelude.Data_List ...
Processing theory HOLCF-Prelude.Data_Maybe ...
Processing theory HOLCF-Prelude.HOLCF_Prelude ...
Processing theory BirdKMP.HOLCF_ROOT ...
Processing theory Noninterference_Sequential_Composition.Propaedeutics ...
Processing theory Noninterference_Sequential_Composition.SequentialComposition ...
Processing theory Noninterference_Sequential_Composition.Counterexamples ...
Processing theory BirdKMP.Theory_Of_Lists ...
Removing 2 theories ...
Processing theory Dependent_SIFUM_Refinement.CompositionalRefinement ...
Processing theory Dependent_SIFUM_Type_Systems.TypeSystem ...
Processing theory Dependent_SIFUM_Type_Systems.TypeSystemTactics ...
Processing theory Dependent_SIFUM_Refinement.Eg1 ...
Processing theory Dependent_SIFUM_Refinement.Eg1Eg2 ...
Processing theory Dependent_SIFUM_Refinement.Eg1Eg2RefinementSimple ...
Loading 6 theories ...
Processing theory BirdKMP.KMP ...
Removing 6 theories ...
Processing theory Dependent_SIFUM_Refinement.Eg1RefinementTrivial ...
Processing theory Collections.SetAbstractionIterator ...
Processing theory Rewriting_Z.Z ...
Processing theory Dependent_SIFUM_Type_Systems.Example_TypeSystem ...
Processing theory Rewriting_Z.Lambda_Z ...
Processing theory Dependent_SIFUM_Type_Systems.Example_Swap_Add ...
Loading 22 theories ...
Processing theory Slicing.ControlDependenceRelations ...
Processing theory Slicing.BitVector ...
Processing theory Slicing.Semantics ...
Processing theory Slicing.WEquivalence ...
Processing theory Slicing.SemanticsWellFormed ...
Processing theory Slicing.DynPDG ...
Processing theory Slicing.StaticControlDependences ...
Removing 20 theories ...
Processing theory Slicing.DynamicControlDependences ...
Processing theory Slicing.DependentLiveVariables ...
Processing theory Slicing.DynSlice ...
Processing theory Stone_Algebras.Filters ...
Processing theory Relational_Minimum_Spanning_Trees.Prim ...
Removing 2 theories ...
Processing theory Stone_Algebras.Stone_Construction ...
Processing theory Stone_Relation_Algebras.Relation_Subalgebras ...
Processing theory Stone_Kleene_Relation_Algebras.Kleene_Relation_Subalgebras ...
Processing theory Slicing.JVMCFG ...
Processing theory Slicing.JVMInterpretation ...
Removing 7 theories ...
Processing theory Slicing.JVMPostdomination ...
Processing theory Slicing.JVMCFG_wf ...
Processing theory Slicing.JVMControlDependences ...
Processing theory Slicing.SemanticsWF ...
Loading 34 theories ...
Processing theory Slicing.Slicing ...
Removing 13 theories ...
Processing theory HOLCF-Prelude.List_Comprehension ...
Processing theory Extended_Finite_State_Machine_Inference.Group_By ...
Processing theory Extended_Finite_State_Machine_Inference.Code_Target_Set ...
Processing theory Extended_Finite_State_Machine_Inference.Code_Target_List ...
Processing theory HOLCF-Prelude.Definedness ...
Processing theory HOLCF-Prelude.Fibs ...
Processing theory HOLCF-Prelude.GHC_Rewrite_Rules ...
Processing theory HOLCF-Prelude.HLint ...
Processing theory Extended_Finite_State_Machine_Inference.Code_Target_FSet ...
Processing theory HOLCF-Prelude.Num_Class ...
Processing theory HOLCF-Prelude.Sieve_Primes ...
Processing theory Extended_Finite_State_Machine_Inference.Subsumption ...
Processing theory Extended_Finite_State_Machines.AExp_Lexorder ...
Processing theory Extended_Finite_State_Machines.GExp_Lexorder ...
Processing theory Extended_Finite_State_Machines.Transition_Lexorder ...
Removing 55 theories ...
Processing theory Extended_Finite_State_Machine_Inference.Inference ...
Processing theory Extended_Finite_State_Machine_Inference.EFSM_Dot ...
Processing theory Extended_Finite_State_Machine_Inference.efsm2sal ...
Processing theory Extended_Finite_State_Machine_Inference.SelectionStrategies ...
Processing theory Extended_Finite_State_Machine_Inference.Distinguishing_Guards ...
Processing theory Extended_Finite_State_Machine_Inference.Increment_Reset ...
Processing theory FOL-Fitting.FOL_Fitting ...
Processing theory FOL_Seq_Calc1.Common ...
Processing theory FOL_Seq_Calc1.Tableau ...
Processing theory FOL_Seq_Calc1.Sequent ...
Processing theory Extended_Finite_State_Machine_Inference.Same_Register ...
Removing 4 theories ...
Processing theory Extended_Finite_State_Machine_Inference.Store_Reuse ...
Processing theory Extended_Finite_State_Machine_Inference.Store_Reuse_Subsumption ...
Processing theory Extended_Finite_State_Machine_Inference.Weak_Subsumption ...
Processing theory Extended_Finite_State_Machine_Inference.Least_Upper_Bound ...
Processing theory Extended_Finite_State_Machine_Inference.PTA_Generalisation ...
Processing theory Extended_Finite_State_Machine_Inference.Code_Generation ...
Processing theory CakeML_Codegen.Test_Embed_Data2 ...
Removing 25 theories ...
Processing theory CakeML_Codegen.Test_Embed_Tree ...
Loading 27 theories ...
Processing theory Goedel_Incompleteness.Abstract_Jeroslow_Encoding ...
Processing theory Relation_Algebra.More_Boolean_Algebra ...
Processing theory Goedel_Incompleteness.Loeb_Formula ...
Processing theory Goedel_Incompleteness.Loeb ...
Processing theory Goedel_Incompleteness.Jeroslow_Simplified ...
Processing theory Goedel_Incompleteness.Rosser_Formula ...
Removing 34 theories ...
Processing theory Goedel_Incompleteness.Tarski ...
Processing theory Goedel_Incompleteness.Abstract_First_Goedel_Rosser ...
Processing theory Polynomials.NZM ...
Processing theory Polynomials.Show_Polynomials ...
Removing 6 theories ...
Processing theory Syntax_Independent_Logic.Pseudo_Term ...
Processing theory Relation_Algebra.Relation_Algebra ...
Processing theory Relation_Algebra.Relation_Algebra_RTC ...
Processing theory Relation_Algebra.Relation_Algebra_Tests ...
Processing theory Relation_Algebra.Relation_Algebra_Vectors ...
Processing theory Goedel_Incompleteness.Jeroslow_Original ...
Processing theory Goedel_Incompleteness.All_Abstract ...
Processing theory Relation_Algebra.Relation_Algebra_Functions ...
Removing 24 theories ...
Processing theory Relational_Paths.More_Relation_Algebra ...
Processing theory Dependent_SIFUM_Refinement.EgHighBranchRevC ...
Removing 2 theories ...
Processing theory Relational_Paths.Paths ...
Processing theory Relational_Paths.Rooted_Paths ...
Processing theory Relational_Paths.Path_Algorithms ...
Loading 32 theories ...
Processing theory Monad_Memo_DP.Ground_Function ...
Processing theory Monad_Memo_DP.Solve_Cong ...
Processing theory Optimal_BST.Quadrilateral_Inequality ...
Processing theory Monad_Memo_DP.Bottom_Up_Computation ...
Processing theory Nominal2.Eqvt ...
Processing theory InformationFlowSlicing.NonInterferenceIntra ...
Processing theory Monad_Memo_DP.Bottom_Up_Computation_Heap ...
Processing theory Nominal2.Atoms ...
Processing theory Monad_Memo_DP.Example_Misc ...
Processing theory Monad_Memo_DP.Index ...
Removing 11 theories ...
Processing theory Optimal_BST.Optimal_BST_Examples ...
Processing theory InformationFlowSlicing.LiftingIntra ...
Processing theory InformationFlowSlicing.NonInterferenceWhile ...
Processing theory Monad_Memo_DP.Counting_Tiles ...
Processing theory LTL_Normal_Form.Normal_Form_Complexity ...
Processing theory Optimal_BST.Weighted_Path_Length ...
Processing theory Monad_Memo_DP.Longest_Common_Subsequence ...
Processing theory Monad_Memo_DP.Pair_Memory ...
Processing theory Monad_Memo_DP.Memory_Heap ...
Removing 36 theories ...
Processing theory Monad_Memo_DP.Heap_Main ...
Processing theory Monad_Memo_DP.Heap_Default ...
Processing theory Monad_Memo_DP.Knapsack ...
Processing theory Monad_Memo_DP.Tracing ...
Processing theory Monad_Memo_DP.OptBST ...
Processing theory Optimal_BST.Optimal_BST ...
Processing theory Monad_Memo_DP.CYK ...
Processing theory Optimal_BST.Optimal_BST2 ...
Processing theory Monad_Memo_DP.Bellman_Ford ...
Processing theory Optimal_BST.Optimal_BST_Code ...
Processing theory Monad_Memo_DP.Min_Ed_Dist0 ...
Loading 13 theories ...
Processing theory Monad_Memo_DP.All_Examples ...
Removing 13 theories ...
Processing theory Containers-Benchmarks.Benchmark_Set_Default ...
Processing theory Optimal_BST.Optimal_BST_Memo ...
Processing theory Kleene_Algebra.Matrix ...
Processing theory Minsky_Machines.Recursive_Inseparability ...
Processing theory Noninterference_Concurrent_Composition.ConcurrentComposition ...
Loading 65 theories ...
Processing theory Minsky_Machines.Minsky ...
Processing theory Auto2_HOL.HOL_Base ...
Processing theory Auto2_HOL.Auto2_HOL ...
Processing theory Auto2_HOL.Logic_Thms ...
Processing theory Auto2_HOL.Order_Thms ...
Processing theory Auto2_HOL.Arith_Thms ...
Processing theory Auto2_HOL.Set_Thms ...
Processing theory Formula_Derivatives.FSet_More ...
Processing theory Auto2_HOL.Lists_Thms ...
Processing theory Auto2_HOL.Auto2_Main ...
Removing 52 theories ...
Processing theory Auto2_Imperative_HOL.Partial_Equiv_Rel ...
Processing theory Auto2_Imperative_HOL.SepLogic_Base ...
Processing theory Auto2_Imperative_HOL.Interval ...
Processing theory Auto2_Imperative_HOL.Mapping_Str ...
Processing theory Auto2_Imperative_HOL.Arrays_Ex ...
Processing theory Auto2_Imperative_HOL.Lists_Ex ...
Processing theory Auto2_Imperative_HOL.BST ...
Processing theory Auto2_Imperative_HOL.Interval_Tree ...
Processing theory Auto2_Imperative_HOL.Quicksort ...
Processing theory Auto2_Imperative_HOL.Dijkstra ...
Processing theory Auto2_Imperative_HOL.Rect_Intersect ...
Processing theory Auto2_Imperative_HOL.Union_Find ...
Processing theory Auto2_Imperative_HOL.Indexed_PQueue ...
Processing theory Auto2_Imperative_HOL.Connectivity ...
Processing theory Auto2_Imperative_HOL.SepAuto ...
Processing theory Auto2_Imperative_HOL.Arrays_Impl ...
Processing theory Formula_Derivatives.WS1S_Prelim ...
Processing theory Auto2_Imperative_HOL.Quicksort_Impl ...
Processing theory Auto2_Imperative_HOL.DynamicArray ...
Processing theory Auto2_Imperative_HOL.GCD_Impl ...
Processing theory Auto2_Imperative_HOL.LinkedList ...
Processing theory Auto2_Imperative_HOL.BST_Impl ...
Processing theory Auto2_Imperative_HOL.RBTree ...
Processing theory Auto2_Imperative_HOL.IntervalTree_Impl ...
Processing theory Auto2_Imperative_HOL.Rect_Intersect_Impl ...
Processing theory Auto2_Imperative_HOL.Union_Find_Impl ...
Processing theory Auto2_Imperative_HOL.Connectivity_Impl ...
Processing theory Extended_Finite_State_Machines.Drinks_Machine_2 ...
Processing theory Extended_Finite_State_Machine_Inference.Drinks_Subsumption ...
Processing theory Auto2_Imperative_HOL.Indexed_PQueue_Impl ...
Processing theory Formula_Derivatives.While_Default ...
Processing theory LTL_Master_Theorem.Asymmetric_Master_Theorem ...
Processing theory Formula_Derivatives.Automaton ...
Processing theory Auto2_Imperative_HOL.Dijkstra_Impl ...
Processing theory Auto2_Imperative_HOL.RBTree_Impl ...
Processing theory Auto2_Imperative_HOL.Sep_Examples ...
Processing theory Nested_Multisets_Ordinals.Unary_PCF ...
Removing 63 theories ...
Removing 7 theories ...
Processing theory Formula_Derivatives.Abstract_Formula ...
Processing theory Formula_Derivatives.WS1S_Formula ...
Processing theory Formula_Derivatives.WS1S_Nameful ...
Processing theory Formula_Derivatives-Examples.WS1S_Nameful_Examples ...
Loading 71 theories ...
Removing 2 theories ...
Processing theory Algebraic_VCs.P2S2R ...
Processing theory Jinja.Hidden ...
Processing theory Quantales.Dioid_Models_New ...
Processing theory Quantales.Quantale_Models ...
Processing theory Jinja.State ...
Processing theory Quantales.Quantic_Nuclei_Conuclei ...
Processing theory Jinja.Expr ...
Processing theory Jinja.Examples ...
Processing theory Jinja.BigStep ...
Processing theory KAT_and_DRA.KAT_Models ...
Processing theory Algebraic_VCs.VC_KAT ...
Processing theory Algebraic_VCs.VC_KAT_Examples ...
Processing theory Algebraic_VCs.VC_KAT_Examples2 ...
Processing theory Algebraic_VCs.RKAT ...
Processing theory Algebraic_VCs.RKAT_Models ...
Processing theory Algebraic_VCs.VC_RKAT ...
Processing theory Algebraic_VCs.VC_RKAT_Examples ...
Processing theory Quantales.Quantale_Left_Sided ...
Processing theory Jinja.J1 ...
Processing theory Jinja.DefAss ...
Processing theory Jinja.WellType ...
Processing theory Jinja.Annotate ...
Removing 10 theories ...
Processing theory Jinja.PCompiler ...
Processing theory Jinja.WellTypeRT ...
Processing theory Jinja.Compiler1 ...
Processing theory Jinja.JVMDefensive ...
Processing theory Jinja.Compiler2 ...
Processing theory Jinja.SmallStep ...
Processing theory Jinja.WWellForm ...
Processing theory Jinja.execute_WellType ...
Processing theory Jinja.Equivalence ...
Processing theory Jinja.JWellForm ...
Processing theory Jinja.Progress ...
Processing theory Jinja.J1WellForm ...
Processing theory Jinja.Correctness1 ...
Processing theory Jinja.execute_Bigstep ...
Processing theory Jinja.TypeSafe ...
Processing theory Formula_Derivatives.Presburger_Formula ...
Processing theory Formula_Derivatives-Examples.WS1S_Examples ...
Processing theory Formula_Derivatives.WS1S_Presburger_Equivalence ...
Processing theory Formula_Derivatives-Examples.WS1S_Presburger_Examples ...
Processing theory Jinja.BVNoTypeError ...
Processing theory Jinja.LBVJVM ...
Processing theory Jinja.Correctness2 ...
Processing theory Jinja.Compiler ...
Removing 4 theories ...
Processing theory Algebraic_VCs.VC_KAD ...
Processing theory Algebraic_VCs.VC_KAD_Examples ...
Processing theory Algebraic_VCs.VC_KAD_Examples2 ...
Processing theory Algebraic_VCs.Pointer_Examples ...
Processing theory Algebraic_VCs.VC_KAD_wf ...
Processing theory Algebraic_VCs.VC_KAD_wf_Examples ...
Processing theory Algebraic_VCs.Path_Model_Example ...
Processing theory Algebraic_VCs.VC_KAD_dual ...
Processing theory Algebraic_VCs.VC_KAD_dual_Examples ...
Processing theory Algebraic_VCs.KAD_is_KAT ...
Removing 16 theories ...
Processing theory Jinja.TypeComp ...
Loading 18 theories ...
Processing theory Jinja.Jinja ...
Processing theory Kleene_Algebra.Finite_Suprema ...
Processing theory Regular_Algebras.Dioid_Power_Sum ...
Processing theory Kleene_Algebra.Omega_Algebra ...
Processing theory Auto2_HOL.Auto2_Test ...
Processing theory Kleene_Algebra.Omega_Algebra_Models ...
Processing theory Complx.Examples ...
Processing theory Residuated_Lattices.Residuated_Lattices ...
Removing 85 theories ...
Processing theory Auto2_HOL.Primes_Ex ...
Processing theory Decreasing-Diagrams-II.Decreasing_Diagrams_II_Aux ...
Processing theory Residuated_Lattices.Action_Algebra ...
Processing theory Residuated_Lattices.Action_Algebra_Models ...
Processing theory Stone_Relation_Algebras.Linear_Order_Matrices ...
Processing theory Decreasing-Diagrams-II.Decreasing_Diagrams_II ...
Processing theory Formula_Derivatives.WS1S_Alt_Formula ...
Removing 27 theories ...
Processing theory Formula_Derivatives-Examples.WS1S_Alt_Examples ...
Removing 7 theories ...
Processing theory Regular_Algebras.Regular_Algebras ...
Loading 32 theories ...
Processing theory Regular_Algebras.Regular_Algebra_Models ...
Processing theory IMP2.IMP2_Utils ...
Processing theory IMP2.Subgoal_Focus_Some ...
Processing theory IMP2.Named_Simpsets ...
Processing theory Regular_Algebras.Pratts_Counterexamples ...
Processing theory IMP2.Syntax ...
Processing theory IMP2.Parser ...
Processing theory Noninterference_Generic_Unwinding.GenericUnwinding ...
Processing theory IMP2.Semantics ...
Processing theory IMP2.Annotated_Syntax ...
Processing theory IMP2.IMP2_Basic_Simpset ...
Processing theory IMP2.IMP2_Basic_Decls ...
Processing theory IMP2.IMP2_Var_Abs ...
Processing theory IMP2.IMP2_Program_Analysis ...
Processing theory IMP2.IMP2_Var_Postprocessor ...
Processing theory IMP2.IMP2_Specification ...
Processing theory IMP2.IMP2_VCG ...
Processing theory Show.Show_Real_Impl ...
Processing theory Nested_Multisets_Ordinals.McCarthy_91 ...
Processing theory Deriving.RBT_Compare_Order_Impl ...
Processing theory Formula_Derivatives-Examples.Presburger_Examples ...
Processing theory Containers-Benchmarks.Benchmark_RBT ...
Processing theory VerifyThis2019.Challenge1A ...
FAILED to process theory VerifyThis2019.Challenge1B
*** Error (line 159 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/VerifyThis2019/Challenge1B.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
Processing theory Quantales.Quantale_Modules ...
Processing theory Regular_Algebras.Regular_Algebra_Variants ...
Removing 44 theories ...
Processing theory IMP2.IMP2_Aux_Lemmas ...
Processing theory Rewriting_Z.CL_Z ...
Processing theory IMP2.IMP2 ...
Processing theory IMP2_Binary_Heap.IMP2_Binary_Heap ...
Processing theory Decreasing-Diagrams.Decreasing_Diagrams ...
Removing 9 theories ...
Processing theory Algebraic_VCs.Domain_Quantale ...
Processing theory IMP2.Examples ...
Loading 70 theories ...
Processing theory IMP2.IMP2_from_IMP ...
Processing theory Interpreter_Optimizations.Dynamic ...
Processing theory Interpreter_Optimizations.List_util ...
Processing theory Interpreter_Optimizations.Op ...
Processing theory Interpreter_Optimizations.OpInl ...
Processing theory IMP2.Quickstart_Guide ...
Processing theory Interpreter_Optimizations.Env ...
Processing theory Interpreter_Optimizations.Option_applicative ...
Processing theory KAT_and_DRA.KAT2 ...
Processing theory Kleene_Algebra.Formal_Power_Series ...
Removing 30 theories ...
Processing theory Kleene_Algebra.Inf_Matrix ...
Processing theory Kleene_Algebra.DRA ...
Processing theory KAT_and_DRA.DRAT2 ...
Processing theory Kleene_Algebra.PHL_DRA ...
Processing theory Residuated_Lattices.Residuated_Boolean_Algebras ...
Processing theory Noninterference_CSP.ClassicalNoninterference ...
Processing theory KAT_and_DRA.DRAT ...
Processing theory KAT_and_DRA.DRA_Models ...
Processing theory KAT_and_DRA.FolkTheorem ...
Processing theory KAT_and_DRA.PHL_DRAT ...
Processing theory Noninterference_CSP.GeneralizedNoninterference ...
Processing theory Ordinal.OrdinalVeblen ...
Processing theory Ordinal.Ordinal ...
Processing theory Relation_Algebra.Relation_Algebra_Direct_Products ...
Processing theory Dependent_SIFUM_Type_Systems.Example ...
Processing theory Relation_Algebra.Relation_Algebra_Models ...
Removing 34 theories ...
Processing theory VeriComp.Behaviour ...
Processing theory VeriComp.Well_founded ...
Processing theory VeriComp.Inf ...
Processing theory VeriComp.Semantics ...
Processing theory VeriComp.Language ...
Processing theory VeriComp.Simulation ...
Processing theory VeriComp.Compiler ...
Processing theory CRDT.Util ...
Processing theory CRDT.Convergence ...
Processing theory Interpreter_Optimizations.Result ...
Processing theory CRDT.Network ...
Processing theory IMAP-CRDT.IMAP-def ...
Processing theory Interpreter_Optimizations.Global ...
Processing theory Residuated_Lattices.Residuated_Relation_Algebra ...
Processing theory UPF.Service ...
Processing theory UPF.ServiceExample ...
Processing theory IMAP-CRDT.IMAP-proof-commute ...
Processing theory Interpreter_Optimizations.Unboxed ...
Processing theory Interpreter_Optimizations.OpUbx ...
Processing theory IMAP-CRDT.IMAP-proof-helpers ...
Processing theory Interpreter_Optimizations.Unboxed_lemmas ...
Processing theory Interpreter_Optimizations.Inca ...
Processing theory Stern_Brocot.Cotree ...
Processing theory Stern_Brocot.Cotree_Algebra ...
Processing theory IMAP-CRDT.IMAP-proof-independent ...
Removing 17 theories ...
Processing theory IMAP-CRDT.IMAP-proof ...
Processing theory HereditarilyFinite.Finitary ...
Processing theory Iptables_Semantics.Alternative_Semantics ...
Processing theory Iptables_Semantics.Semantics_Stateful ...
Processing theory HereditarilyFinite.Finite_Automata ...
Processing theory Multirelations.C_Algebras ...
Processing theory Interpreter_Optimizations.Ubx ...
Processing theory Interpreter_Optimizations.Ubx_type_inference ...
Processing theory Card_Equiv_Relations.Card_Equiv_Relations ...
Removing 27 theories ...
Processing theory Card_Equiv_Relations.Card_Partial_Equiv_Relations ...
Processing theory Interpreter_Optimizations.Inca_to_Ubx_simulation ...
Processing theory Stern_Brocot.Stern_Brocot_Tree ...
Processing theory Stern_Brocot.Bird_Tree ...
Processing theory Interpreter_Optimizations.Inca_to_Ubx_compiler ...
Removing 10 theories ...
Processing theory Multirelations.Multirelations ...
Loading 81 theories ...
Processing theory Automatic_Refinement.Param_Chapter ...
Processing theory Automatic_Refinement.Autoref_Chapter ...
Processing theory Applicative_Lifting.Joinable ...
Processing theory CakeML.Doc_Generated ...
Processing theory CakeML.Doc_Proofs ...
Processing theory CakeML_Codegen.Doc_Backend ...
Processing theory CakeML_Codegen.Doc_Compiler ...
Processing theory CakeML_Codegen.Doc_CupCake ...
Processing theory CakeML_Codegen.Doc_Preproc ...
Processing theory CakeML_Codegen.Doc_Rewriting ...
Processing theory CakeML_Codegen.Doc_Terms ...
Processing theory Collections.Collections_Entrypoints_Chapter ...
Processing theory Collections_Examples.Collection_Autoref_Examples_Chapter ...
Processing theory Collections_Examples.Examples_Chapter ...
Processing theory Collections_Examples.ICF_Examples_Chapter ...
Processing theory Collections_Examples.Refine_Monadic_Examples_Chapter ...
Processing theory Collections.GenCF_Gen_Chapter ...
Processing theory Collections.GenCF_Chapter ...
Processing theory Collections.GenCF_Intf_Chapter ...
Processing theory Collections.ICF_Chapter ...
Processing theory Collections.GenCF_Impl_Chapter ...
Processing theory Collections.ICF_Entrypoints_Chapter ...
Processing theory Collections.ICF_Gen_Algo_Chapter ...
Processing theory Collections.ICF_Impl_Chapter ...
Processing theory Collections.ICF_Spec_Chapter ...
Processing theory Collections.Userguides_Chapter ...
Processing theory DFS_Framework.DFS_Chapter_Framework ...
Processing theory DFS_Framework.DFS_Chapter_Examples ...
Processing theory Dijkstra_Shortest_Path.Introduction ...
Processing theory Auto2_HOL.Pelletier ...
Processing theory IMO2019.IMO2019_Q1 ...
Processing theory Prim_Dijkstra_Simple.Chapter_Dijkstra ...
Processing theory Prim_Dijkstra_Simple.Chapter_Prim ...
Processing theory Refine_Imperative_HOL.Sepref_Chapter_Examples ...
Processing theory Refine_Imperative_HOL.Sepref_Chapter_IICF ...
Processing theory Refine_Imperative_HOL.Sepref_Chapter_Setup ...
Processing theory Refine_Imperative_HOL.Sepref_Chapter_Tool ...
Processing theory Refine_Imperative_HOL.Sepref_Chapter_Userguides ...
Processing theory Refine_Imperative_HOL.Sepref_Chapter_Benchmarks ...
Processing theory Iptables_Semantics.Negation_Type_DNF ...
Processing theory Interpreter_Optimizations.Env_list ...
Processing theory Algebraic_VCs.VC_KAT_scratch ...
Removing 48 theories ...
Processing theory Sturm_Sequences.Sturm_Library_Document ...
Processing theory Transitive-Closure.Finite_Transitive_Closure_Simprocs ...
Processing theory VeriComp.Fixpoint ...
Processing theory Residuated_Lattices.Involutive_Residuated ...
Processing theory Algebraic_VCs.VC_KAD_scratch ...
Processing theory Regular-Sets.Regular_Exp2 ...
Processing theory Applicative_Lifting.Abstract_AF ...
Processing theory BTree.BTree_Height ...
Processing theory CRDT.Counter ...
Processing theory Dependent_SIFUM_Type_Systems.LocallySoundModeUse ...
Processing theory Posix-Lexing.Lexer ...
Removing 19 theories ...
Processing theory CRDT.ORSet ...
Processing theory CRDT.Ordered_List ...
Processing theory Posix-Lexing.Simplifying ...
Processing theory Containers-Benchmarks.Benchmark_Default ...
Processing theory Interpreter_Optimizations.Op_example ...
Processing theory Interpreter_Optimizations.Std ...
Processing theory Interpreter_Optimizations.Std_to_Inca_simulation ...
Processing theory Interpreter_Optimizations.Std_to_Inca_compiler ...
Processing theory CRDT.RGA ...
Removing 38 theories ...
Processing theory Applicative_Lifting.Applicative_Test ...
Processing theory Order_Lattice_Props.Order_Lattice_Props_Wenzel ...
Processing theory Containers.Card_Datatype_Ex ...
Processing theory Order_Lattice_Props.Representations ...
Processing theory Regular-Sets.Regexp_Constructions ...
Processing theory Regular-Sets.pEquivalence_Checking ...
Processing theory Order_Lattice_Props.Order_Lattice_Props_Loc ...
Removing 31 theories ...
Processing theory Applicative_Lifting.Beta_Eta ...
Processing theory Applicative_Lifting.Combinators ...
Processing theory Applicative_Lifting.Idiomatic_Terms ...
Processing theory Regular-Sets.Equivalence_Checking2 ...
Removing 12 theories ...
Processing theory Subset_Boolean_Algebras.Subset_Boolean_Algebras ...
*** FAILED theory Topological_Semantics.topo_operators_basic
*** Error (line 114 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/topo_operators_basic.thy"):
*** Unexpected outcome: "unknown"
*** 
*** FAILED theory Topological_Semantics.sse_operation_negative
*** Error (line 260 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/sse_operation_negative.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 261 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/sse_operation_negative.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 263 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/sse_operation_negative.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 292 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/sse_operation_negative.thy"):
*** Failed to apply initial proof method⌂:
*** using this:
***     ECQw ?η ≡ ∀a b. ?η b ❙≽ a ❙∧ ?η a
***     TNDw ?η ≡ ∀φ b. φ ❙∨ ?η φ ❙≽ ?η b
***     atom ?a ≡ ¬ (∀w. ?a w = ❙⊥ w) ∧ (∀p. p ❙≽ ?a ∨ ❙─p ❙≽ ?a)
***     ∀w. ∃q. q w ∧ atom q
***     ?A ❙∧ ?B ≡ λw. ?A w ∧ ?B w
***     ?A ❙∨ ?B ≡ λw. ?A w ∨ ?B w
***     ❙⊤ ≡ λw. True
***     ❙⊥ ≡ λw. False
***     ?A ❙→ ?B ≡ λw. ?A w ⟶ ?B w
***     ?A ❙↔ ?B ≡ λw. ?A w = ?B w
***     ?A ❙↼ ?B ≡ λw. ?A w ∧ ¬ ?B w
***     ❙─?A ≡ λw. ¬ ?A w
*** goal (1 subgoal):
***  1. ∀a b c. b ❙≽ (λw. c w ∧ a w) ⟶ η a ❙≽ (λw. c w ∧ η b w) ⟹
***     ∀a b. (λw. η a w ∨ η b w) ❙≽ η (λw. a w ∧ b w)
*** Error (line 293 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/sse_operation_negative.thy"):
*** Bad context for command "lemma"⌂ -- using reset state
*** 
*** FAILED theory Topological_Semantics.topo_strict_implication
*** Error (line 96 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/topo_strict_implication.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 106 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/topo_strict_implication.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 107 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/topo_strict_implication.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 112 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/topo_strict_implication.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 113 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/topo_strict_implication.thy"):
*** Unexpected outcome: "unknown"
*** 
*** FAILED theory Topological_Semantics.topo_negation_conditions
*** Error (line 55 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/topo_negation_conditions.thy"):
*** Unexpected outcome: "unknown"
*** 
*** FAILED theory Topological_Semantics.ex_subminimal_logics
*** Error (line 82 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_subminimal_logics.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 88 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_subminimal_logics.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 109 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_subminimal_logics.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 199 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_subminimal_logics.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 201 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_subminimal_logics.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 208 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_subminimal_logics.thy"):
*** Unexpected outcome: "unknown"
*** 
*** FAILED theory Topological_Semantics.ex_LFIs
*** Error (line 127 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_LFIs.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 128 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_LFIs.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 137 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_LFIs.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 138 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_LFIs.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 148 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_LFIs.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 149 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_LFIs.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 153 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_LFIs.thy"):
*** Unexpected outcome: "unknown"
*** 
*** FAILED theory Topological_Semantics.topo_operators_derivative
*** Error (line 97 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/topo_operators_derivative.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 114 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/topo_operators_derivative.thy"):
*** Unexpected outcome: "unknown"
*** 
*** FAILED theory Topological_Semantics.topo_derivative_algebra
*** Error (line 90 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/topo_derivative_algebra.thy"):
*** Unexpected outcome: "unknown"
*** 
*** FAILED theory Topological_Semantics.ex_LFUs
*** Error (line 53 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_LFUs.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 56 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_LFUs.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 58 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_LFUs.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 59 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_LFUs.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 72 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_LFUs.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 81 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_LFUs.thy"):
*** Unexpected outcome: "unknown"
*** 
*** FAILED theory Topological_Semantics.topo_border_algebra
*** Error (line 47 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/topo_border_algebra.thy"):
*** Unexpected outcome: "unknown"
*** 
*** FAILED theory Topological_Semantics.topo_closure_algebra
*** Error (line 46 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/topo_closure_algebra.thy"):
*** Unexpected outcome: "unknown"
*** 
*** FAILED theory Topological_Semantics.topo_interior_algebra
*** Error (line 46 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/topo_interior_algebra.thy"):
*** Unexpected outcome: "unknown"
*** 
*** FAILED theory Collections.ArrayMapImpl
*** Error (line 360 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/ICF/impl/ArrayMapImpl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Collections.ListMapImpl
*** Error (line 101 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/ICF/impl/ListMapImpl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Collections.TrieMapImpl
*** Error (line 163 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/ICF/impl/TrieMapImpl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Collections.ListSetImpl
*** Error (line 120 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/ICF/impl/ListSetImpl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Collections.ListSetImpl_Invar
*** Error (line 105 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/ICF/impl/ListSetImpl_Invar.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Collections.TrieSetImpl
*** Error (line 77 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/ICF/impl/TrieSetImpl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Collections.ListSetImpl_NotDist
*** Error (line 202 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/ICF/impl/ListSetImpl_NotDist.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Collections.ArrayHashMap
*** Error (line 168 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/ICF/impl/ArrayHashMap.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Collections.ArrayHashSet
*** Error (line 77 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/ICF/impl/ArrayHashSet.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Collections.RBTMapImpl
*** Error (line 135 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/ICF/impl/RBTMapImpl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Collections.HashMap
*** Error (line 201 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/ICF/impl/HashMap.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Collections.RBTSetImpl
*** Error (line 102 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/ICF/impl/RBTSetImpl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory CAVA_LTL_Modelchecker.NDFS_SI_Statistics
*** Error (line 81 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_LTL_Modelchecker/Nested_DFS/NDFS_SI_Statistics.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory CAVA_Automata.Digraph_Impl
*** Error (line 381 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_Automata/Digraph_Impl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Gabow_SCC.Find_Path_Impl
*** Error (line 345 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Gabow_SCC/Find_Path_Impl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory SM.Rename_Cfg
*** Error (line 733 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_LTL_Modelchecker/SM/Refine/Rename_Cfg.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Gabow_SCC.Gabow_Skeleton_Code
*** Error (line 269 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Gabow_SCC/Gabow_Skeleton_Code.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory CAVA_LTL_Modelchecker.NDFS_SI
*** Error (line 1309 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_LTL_Modelchecker/Nested_DFS/NDFS_SI.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 1336 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_LTL_Modelchecker/Nested_DFS/NDFS_SI.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 1361 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_LTL_Modelchecker/Nested_DFS/NDFS_SI.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 1394 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_LTL_Modelchecker/Nested_DFS/NDFS_SI.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 1423 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_LTL_Modelchecker/Nested_DFS/NDFS_SI.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 1454 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_LTL_Modelchecker/Nested_DFS/NDFS_SI.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 1537 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_LTL_Modelchecker/Nested_DFS/NDFS_SI.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Gabow_SCC.Gabow_GBG_Code
*** Error (line 320 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Gabow_SCC/Gabow_GBG_Code.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory DFS_Framework.Reachable_Nodes
*** Error (line 205 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/DFS_Framework/Examples/Reachable_Nodes.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 262 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/DFS_Framework/Examples/Reachable_Nodes.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory DFS_Framework.Feedback_Arcs
*** Error (line 388 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/DFS_Framework/Examples/Feedback_Arcs.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory SM.SM_Ample_Impl
*** Error (line 494 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_LTL_Modelchecker/SM/Impl/SM_Ample_Impl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 527 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_LTL_Modelchecker/SM/Impl/SM_Ample_Impl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 1298 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_LTL_Modelchecker/SM/Impl/SM_Ample_Impl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory CAVA_LTL_Modelchecker.CAVA_Impl
*** Error (line 832 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_LTL_Modelchecker/CAVA_Impl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 1506 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CAVA_LTL_Modelchecker/CAVA_Impl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Flow_Networks.NetCheck
*** Error (line 708 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Flow_Networks/NetCheck.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 1511 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Flow_Networks/NetCheck.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Prpu_Maxflow.Relabel_To_Front_Impl
*** Error (line 413 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Prpu_Maxflow/Relabel_To_Front_Impl.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 494 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Prpu_Maxflow/Relabel_To_Front_Impl.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Prpu_Maxflow.Fifo_Push_Relabel_Impl
*** Error (line 803 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Prpu_Maxflow/Fifo_Push_Relabel_Impl.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 893 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Prpu_Maxflow/Fifo_Push_Relabel_Impl.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 996 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Prpu_Maxflow/Fifo_Push_Relabel_Impl.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory EdmondsKarp_Maxflow.Augmenting_Path_BFS
*** Error (line 731 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/EdmondsKarp_Maxflow/Augmenting_Path_BFS.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory EdmondsKarp_Maxflow.EdmondsKarp_Impl
*** Error (line 983 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/EdmondsKarp_Maxflow/EdmondsKarp_Impl.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory EdmondsKarp_Maxflow.Edka_Checked_Impl
*** Error (line 53 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/EdmondsKarp_Maxflow/Edka_Checked_Impl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory VerifyThis2019.Challenge2A
*** Error (line 275 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/VerifyThis2019/Challenge2A.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory VerifyThis2018.Snippets
*** Error (line 79 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/VerifyThis2018/Snippets.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 112 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/VerifyThis2018/Snippets.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 162 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/VerifyThis2018/Snippets.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Collections_Examples.Succ_Graph
*** Error (line 74 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/Examples/Autoref/Succ_Graph.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 89 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/Examples/Autoref/Succ_Graph.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Refine_Imperative_HOL.Sepref_Graph
*** Error (line 79 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Refine_Imperative_HOL/Examples/Sepref_Graph.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Refine_Imperative_HOL.Sepref_DFS
*** Error (line 233 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Refine_Imperative_HOL/Examples/Sepref_DFS.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Refine_Imperative_HOL.Sepref_WGraph
*** Error (line 89 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Refine_Imperative_HOL/Examples/Sepref_WGraph.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Refine_Imperative_HOL.Sepref_Minitests
*** Error (line 309 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Refine_Imperative_HOL/Examples/Sepref_Minitests.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 334 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Refine_Imperative_HOL/Examples/Sepref_Minitests.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 344 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Refine_Imperative_HOL/Examples/Sepref_Minitests.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 395 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Refine_Imperative_HOL/Examples/Sepref_Minitests.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Collections_Examples.Nested_DFS
*** Error (line 1100 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/Examples/Autoref/Nested_DFS.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Refine_Imperative_HOL.Sepref_NDFS
*** Error (line 62 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Refine_Imperative_HOL/Examples/Sepref_NDFS.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 113 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Refine_Imperative_HOL/Examples/Sepref_NDFS.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 161 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Refine_Imperative_HOL/Examples/Sepref_NDFS.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Dijkstra_Shortest_Path.Dijkstra_Impl_Adet
*** Error (line 392 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Dijkstra_Shortest_Path/Dijkstra_Impl_Adet.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 400 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Dijkstra_Shortest_Path/Dijkstra_Impl_Adet.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Refine_Imperative_HOL.Sepref_Dijkstra
*** Error (line 230 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Refine_Imperative_HOL/Examples/Sepref_Dijkstra.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Floyd_Warshall.FW_Code
*** Error (line 106 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Floyd_Warshall/FW_Code.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Refine_Imperative_HOL.Sepref_Guide_Quickstart
*** Error (line 132 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Refine_Imperative_HOL/Userguides/Sepref_Guide_Quickstart.thy"):
*** Code check failed for SML_imp: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 271 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Refine_Imperative_HOL/Userguides/Sepref_Guide_Quickstart.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory DFS_Framework.Cyc_Check
*** Error (line 471 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/DFS_Framework/Examples/Cyc_Check.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory DFS_Framework.DFS_Find_Path
*** Error (line 648 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/DFS_Framework/Examples/DFS_Find_Path.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory DFS_Framework.Nested_DFS
*** Error (line 940 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/DFS_Framework/Examples/Nested_DFS.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Containers.Containers_TwoSat_Ex
*** Error (line 236 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Containers/Examples/Containers_TwoSat_Ex.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 250 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Containers/Examples/Containers_TwoSat_Ex.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 320 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Containers/Examples/Containers_TwoSat_Ex.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Prim_Dijkstra_Simple.Prim_Impl
*** Error (line 451 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Prim_Dijkstra_Simple/Prim_Impl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Collections_Examples.PerformanceTest
*** Error (line 114 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/Examples/ICF/PerformanceTest.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Collections_Examples.Simple_DFS
*** Error (line 297 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/Examples/Autoref/Simple_DFS.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 419 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/Examples/Autoref/Simple_DFS.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Collections_Examples.Foreach_Refine
*** Error (line 122 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/Examples/Refine_Monadic/Foreach_Refine.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Collections_Examples.Combined_TwoSat
*** Error (line 171 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/Examples/Autoref/Combined_TwoSat.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 173 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/Examples/Autoref/Combined_TwoSat.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Collections_Examples.itp_2010
*** Error (line 53 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/Examples/ICF/itp_2010.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Collections_Examples.Coll_Test
*** Error (line 462 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/Examples/Autoref/Coll_Test.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Collections_Examples.Bfs_Impl
*** Error (line 174 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/Examples/Refine_Monadic/Bfs_Impl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Containers.Map_To_Mapping_Ex
*** Error (line 21 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Containers/Examples/Map_To_Mapping_Ex.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Dijkstra_Shortest_Path.Dijkstra_Impl
*** Error (line 231 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Dijkstra_Shortest_Path/Dijkstra_Impl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Simple_Firewall.GroupF
*** Error (line 54 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Simple_Firewall/Common/GroupF.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory IP_Addresses.IP_Address
*** Error (line 401 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/IP_Addresses/IP_Address.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory CakeML_Codegen.Test_Utils
*** Error (line 65 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CakeML_Codegen/Utils/Test_Utils.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 67 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CakeML_Codegen/Utils/Test_Utils.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 75 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CakeML_Codegen/Utils/Test_Utils.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 83 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/CakeML_Codegen/Utils/Test_Utils.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Collections.Refine_Monadic_Userguide
*** Error (line 458 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/Userguides/Refine_Monadic_Userguide.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 530 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/Userguides/Refine_Monadic_Userguide.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Prim_Dijkstra_Simple.Dijkstra_Impl
*** Error (line 279 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Prim_Dijkstra_Simple/Dijkstra_Impl.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Native_Word.Native_Word_Test
*** Error (line 68 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Native_Word/Native_Word_Test.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 221 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Native_Word/Native_Word_Test.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 319 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Native_Word/Native_Word_Test.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 410 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Native_Word/Native_Word_Test.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 445 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Native_Word/Native_Word_Test.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Native_Word.Native_Word_Test_Emu
*** Error (line 22 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Native_Word/Native_Word_Test_Emu.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** Error (line 52 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Native_Word/Native_Word_Test_Emu.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory Collections.Locale_Code_Ex
*** Error (line 88 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Collections/ICF/tools/Locale_Code_Ex.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** 
*** FAILED theory VerifyThis2019.Challenge1B
*** Error (line 159 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/VerifyThis2019/Challenge1B.thy"):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure
+ true