Tobias

On 06/12/2017 15:48, Lawrence Paulson wrote:

I've just updated to a recent version (fa1173288322) and tried to run a session by the following command: isabelle jedit -l HOL-Analysis CV.thy And then I get an alert box containing the appended text. Any idea what's going wrong here? Larry Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Markov_Models/Probability.thy" The error(s) above occurred for theory "Markov_Models.Probability" (required by "Markov_Models.Markov_Models" via "Markov_Models.Markov_Models_Auxiliary") (line 9 of "/Users/lp15/isabelle/afp/devel/thys/Markov_Models/Markov_Models_Auxiliary.thy") No such file: "/Users/lp15/isabelle/afp/devel/thys/Markov_Models/Probability.thy" The error(s) above occurred in session "Markov_Models" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Markov_Models/ROOT") [ line 12 of "/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_KBOs/Lambda_Free_KBO_App.thy"] error: keyword "begin" expected, but string was found: "\<ge>t" ^ The error(s) above occurred for theory "Lambda_Free_KBOs.Lambda_Free_KBO_App" (required by "Lambda_Free_KBOs.Lambda_Free_KBOs") (line 12 of "/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_KBOs/Lambda_Free_KBOs.thy") [ line 15 of "/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_KBOs/Lambda_Free_KBO_Std.thy"] error: keyword "begin" expected, but string was found: "\<ge>t" ^ The error(s) above occurred for theory "Lambda_Free_KBOs.Lambda_Free_KBO_Std" (required by "Lambda_Free_KBOs.Lambda_Free_KBOs" via "Lambda_Free_KBOs.Lambda_Free_KBO_Basic") (line 9 of "/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_KBOs/Lambda_Free_KBO_Basic.thy") [ line 16 of "/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_KBOs/Lambda_Free_TKBO_Coefs.thy"] error: keyword "begin" expected, but string was found: ">p" ^ The error(s) above occurred for theory "Lambda_Free_KBOs.Lambda_Free_TKBO_Coefs" (required by "Lambda_Free_KBOs.Lambda_Free_KBOs") (line 12 of "/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_KBOs/Lambda_Free_KBOs.thy") The error(s) above occurred in session "Lambda_Free_KBOs" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_KBOs/ROOT") Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/MFMC_Countable/Probability.thy" The error(s) above occurred for theory "MFMC_Countable.Probability" (required by "Probabilistic_While.While_SPMF" via "MFMC_Countable.Rel_PMF_Characterisation" via "MFMC_Countable.Matrix_For_Marginals" via "MFMC_Countable.MFMC_Misc") (line 6 of "/Users/lp15/isabelle/afp/devel/thys/MFMC_Countable/MFMC_Misc.thy") Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Probabilistic_While/Probability.thy" The error(s) above occurred for theory "Probabilistic_While.Probability" (required by "Probabilistic_While.Bernoulli") (line 8 of "/Users/lp15/isabelle/afp/devel/thys/Probabilistic_While/Bernoulli.thy") No such file: "/Users/lp15/isabelle/afp/devel/thys/MFMC_Countable/Probability.thy" No such file: "/Users/lp15/isabelle/afp/devel/thys/Probabilistic_While/Probability.thy" The error(s) above occurred in session "Probabilistic_While" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Probabilistic_While/ROOT") Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Probabilistic_System_Zoo/Probability.thy" The error(s) above occurred for theory "Probabilistic_System_Zoo.Probability" (required by "Probabilistic_System_Zoo.Probabilistic_Hierarchy") (line 5 of "/Users/lp15/isabelle/afp/devel/thys/Probabilistic_System_Zoo/Probabilistic_Hierarchy.thy") No such file: "/Users/lp15/isabelle/afp/devel/thys/Probabilistic_System_Zoo/Probability.thy" The error(s) above occurred in session "Probabilistic_System_Zoo" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Probabilistic_System_Zoo/ROOT") Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Randomised_Social_Choice/Probability.thy" The error(s) above occurred for theory "Randomised_Social_Choice.Probability" (required by "Randomised_Social_Choice.Randomised_Social_Choice" via "Randomised_Social_Choice.SDS_Lowering" via "Randomised_Social_Choice.Social_Decision_Schemes") (line 13 of "/Users/lp15/isabelle/afp/devel/thys/Randomised_Social_Choice/Social_Decision_Schemes.thy") No such file: "/Users/lp15/isabelle/afp/devel/thys/Randomised_Social_Choice/Probability.thy" The error(s) above occurred in session "Randomised_Social_Choice" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Randomised_Social_Choice/ROOT") Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Quick_Sort_Cost/Probability.thy" The error(s) above occurred for theory "Quick_Sort_Cost.Probability" (required by "Quick_Sort_Cost.Randomised_Quick_Sort") (line 10 of "/Users/lp15/isabelle/afp/devel/thys/Quick_Sort_Cost/Randomised_Quick_Sort.thy") No such file: "/Users/lp15/isabelle/afp/devel/thys/Quick_Sort_Cost/Probability.thy" The error(s) above occurred in session "Quick_Sort_Cost" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Quick_Sort_Cost/ROOT") Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Monad_Normalisation/Probability.thy" The error(s) above occurred for theory "Monad_Normalisation.Probability" (required by "CryptHOL.Misc_CryptHOL" via "Monad_Normalisation.Monad_Normalisation") (line 12 of "/Users/lp15/isabelle/afp/devel/thys/Monad_Normalisation/Monad_Normalisation.thy") Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Monomorphic_Monad/Probability.thy" The error(s) above occurred for theory "Monomorphic_Monad.Probability" (required by "CryptHOL.Misc_CryptHOL" via "Monomorphic_Monad.Monomorphic_Monad") (line 5 of "/Users/lp15/isabelle/afp/devel/thys/Monomorphic_Monad/Monomorphic_Monad.thy") Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Applicative_Lifting/Probability.thy" The error(s) above occurred for theory "Applicative_Lifting.Probability" (required by "CryptHOL.SPMF_Applicative" via "Applicative_Lifting.Applicative_PMF") (line 7 of "/Users/lp15/isabelle/afp/devel/thys/Applicative_Lifting/Applicative_PMF.thy") No such file: "/Users/lp15/isabelle/afp/devel/thys/Monad_Normalisation/Probability.thy" No such file: "/Users/lp15/isabelle/afp/devel/thys/Monomorphic_Monad/Probability.thy" No such file: "/Users/lp15/isabelle/afp/devel/thys/Applicative_Lifting/Probability.thy" The error(s) above occurred in session "CryptHOL" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/CryptHOL/ROOT") [ line 7 of "/Users/lp15/isabelle/afp/devel/thys/HereditarilyFinite/HF.thy"] error: keyword "begin" expected, but string was found: "~<:" ^ The error(s) above occurred for theory "HereditarilyFinite.HF" (required by "Finite_Automata_HF.Finite_Automata_HF" via "HereditarilyFinite.Ordinal") (line 3 of "/Users/lp15/isabelle/afp/devel/thys/HereditarilyFinite/Ordinal.thy") The error(s) above occurred in session "Finite_Automata_HF" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Finite_Automata_HF/ROOT") [ line 7 of "/Users/lp15/isabelle/afp/devel/thys/HereditarilyFinite/HF.thy"] error: keyword "begin" expected, but string was found: "~<:" ^ The error(s) above occurred for theory "HereditarilyFinite.HF" (required by "HereditarilyFinite.Rank" via "HereditarilyFinite.Ordinal") (line 3 of "/Users/lp15/isabelle/afp/devel/thys/HereditarilyFinite/Ordinal.thy") The error(s) above occurred in session "HereditarilyFinite" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/HereditarilyFinite/ROOT") Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Monomorphic_Monad/Probability.thy" The error(s) above occurred for theory "Monomorphic_Monad.Probability" (required by "Monomorphic_Monad.Monomorphic_Monad") (line 5 of "/Users/lp15/isabelle/afp/devel/thys/Monomorphic_Monad/Monomorphic_Monad.thy") No such file: "/Users/lp15/isabelle/afp/devel/thys/Monomorphic_Monad/Probability.thy" The error(s) above occurred in session "Monomorphic_Monad" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Monomorphic_Monad/ROOT") Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Buffons_Needle/Probability.thy" The error(s) above occurred for theory "Buffons_Needle.Probability" (required by "Buffons_Needle.Buffons_Needle") (line 9 of "/Users/lp15/isabelle/afp/devel/thys/Buffons_Needle/Buffons_Needle.thy") No such file: "/Users/lp15/isabelle/afp/devel/thys/Buffons_Needle/Probability.thy" The error(s) above occurred in session "Buffons_Needle" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Buffons_Needle/ROOT") Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Applicative_Lifting/Probability.thy" The error(s) above occurred for theory "Applicative_Lifting.Probability" (required by "Applicative_Lifting.Applicative_Functor" via "Applicative_Lifting.Applicative_PMF") (line 7 of "/Users/lp15/isabelle/afp/devel/thys/Applicative_Lifting/Applicative_PMF.thy") No such file: "/Users/lp15/isabelle/afp/devel/thys/Applicative_Lifting/Probability.thy" The error(s) above occurred in session "Applicative_Lifting" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Applicative_Lifting/ROOT") Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Density_Compiler/Probability.thy" The error(s) above occurred for theory "Density_Compiler.Probability" (required by "Density_Compiler.PDF_Transformations" via "Density_Compiler.Density_Predicates") (line 9 of "/Users/lp15/isabelle/afp/devel/thys/Density_Compiler/Density_Predicates.thy") No such file: "/Users/lp15/isabelle/afp/devel/thys/Density_Compiler/Probability.thy" The error(s) above occurred in session "Density_Compiler" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Density_Compiler/ROOT") Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Girth_Chromatic/Probability.thy" The error(s) above occurred for theory "Girth_Chromatic.Probability" (required by "Girth_Chromatic.Girth_Chromatic") (line 5 of "/Users/lp15/isabelle/afp/devel/thys/Girth_Chromatic/Girth_Chromatic.thy") No such file: "/Users/lp15/isabelle/afp/devel/thys/Girth_Chromatic/Probability.thy" The error(s) above occurred in session "Girth_Chromatic" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Girth_Chromatic/ROOT") Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Ergodic_Theory/Probability.thy" The error(s) above occurred for theory "Ergodic_Theory.Probability" (required by "Ergodic_Theory.SG_Library_Complement") (line 6 of "/Users/lp15/isabelle/afp/devel/thys/Ergodic_Theory/SG_Library_Complement.thy") No such file: "/Users/lp15/isabelle/afp/devel/thys/Ergodic_Theory/Probability.thy" The error(s) above occurred in session "Ergodic_Theory" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Ergodic_Theory/ROOT") Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Ergodic_Theory/Probability.thy" The error(s) above occurred for theory "Ergodic_Theory.Probability" (required by "Lp.Functional_Spaces" via "Ergodic_Theory.SG_Library_Complement") (line 6 of "/Users/lp15/isabelle/afp/devel/thys/Ergodic_Theory/SG_Library_Complement.thy") No such file: "/Users/lp15/isabelle/afp/devel/thys/Ergodic_Theory/Probability.thy" The error(s) above occurred in session "Lp" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Lp/ROOT") Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Random_Graph_Subgraph_Threshold/Probability.thy" The error(s) above occurred for theory "Random_Graph_Subgraph_Threshold.Probability" (required by "Random_Graph_Subgraph_Threshold.Subgraph_Threshold" via "Random_Graph_Subgraph_Threshold.Ugraph_Properties" via "Random_Graph_Subgraph_Threshold.Ugraph_Lemmas" via "Random_Graph_Subgraph_Threshold.Prob_Lemmas") (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Random_Graph_Subgraph_Threshold/Prob_Lemmas.thy") No such file: "/Users/lp15/isabelle/afp/devel/thys/Random_Graph_Subgraph_Threshold/Probability.thy" The error(s) above occurred in session "Random_Graph_Subgraph_Threshold" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Random_Graph_Subgraph_Threshold/ROOT") Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Markov_Models/Probability.thy" The error(s) above occurred for theory "Markov_Models.Probability" (required by "Probabilistic_Noninterference.Interface" via "Markov_Models.Discrete_Time_Markov_Chain" via "Markov_Models.Markov_Models_Auxiliary") (line 9 of "/Users/lp15/isabelle/afp/devel/thys/Markov_Models/Markov_Models_Auxiliary.thy") No such file: "/Users/lp15/isabelle/afp/devel/thys/Markov_Models/Probability.thy" The error(s) above occurred in session "Probabilistic_Noninterference" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Probabilistic_Noninterference/ROOT") Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Fisher_Yates/Probability.thy" The error(s) above occurred for theory "Fisher_Yates.Probability" (required by "Fisher_Yates.Fisher_Yates") (line 11 of "/Users/lp15/isabelle/afp/devel/thys/Fisher_Yates/Fisher_Yates.thy") No such file: "/Users/lp15/isabelle/afp/devel/thys/Fisher_Yates/Probability.thy" The error(s) above occurred in session "Fisher_Yates" (line 2 of "/Users/lp15/isabelle/afp/devel/thys/Fisher_Yates/ROOT") Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/List_Update/Probability.thy" The error(s) above occurred for theory "List_Update.Probability" (required by "List_Update.Move_to_Front" via "List_Update.Competitive_Analysis" via "List_Update.Prob_Theory") (line 8 of "/Users/lp15/isabelle/afp/devel/thys/List_Update/Prob_Theory.thy") No such file: "/Users/lp15/isabelle/afp/devel/thys/List_Update/Probability.thy" The error(s) above occurred in session "List_Update" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/List_Update/ROOT") Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Monad_Normalisation/Probability.thy" The error(s) above occurred for theory "Monad_Normalisation.Probability" (required by "Monad_Normalisation.Monad_Normalisation") (line 12 of "/Users/lp15/isabelle/afp/devel/thys/Monad_Normalisation/Monad_Normalisation.thy") No such file: "/Users/lp15/isabelle/afp/devel/thys/Monad_Normalisation/Probability.thy" The error(s) above occurred in session "Monad_Normalisation" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Monad_Normalisation/ROOT") Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Probabilistic_System_Zoo/Probability.thy" The error(s) above occurred for theory "Probabilistic_System_Zoo-Non_BNFs.Probability" (required by "Probabilistic_System_Zoo-Non_BNFs.Probabilistic_Hierarchy") (line 5 of "/Users/lp15/isabelle/afp/devel/thys/Probabilistic_System_Zoo/Probabilistic_Hierarchy.thy") No such file: "/Users/lp15/isabelle/afp/devel/thys/Probabilistic_System_Zoo/Probability.thy" The error(s) above occurred in session "Probabilistic_System_Zoo-Non_BNFs" (line 28 of "/Users/lp15/isabelle/afp/devel/thys/Probabilistic_System_Zoo/ROOT") Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/MFMC_Countable/Probability.thy" The error(s) above occurred for theory "MFMC_Countable.Probability" (required by "MFMC_Countable.Max_Flow_Min_Cut_Countable" via "MFMC_Countable.MFMC_Misc") (line 6 of "/Users/lp15/isabelle/afp/devel/thys/MFMC_Countable/MFMC_Misc.thy") No such file: "/Users/lp15/isabelle/afp/devel/thys/MFMC_Countable/Probability.thy" The error(s) above occurred in session "MFMC_Countable" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/MFMC_Countable/ROOT") [ line 12 of "/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_RPOs/Lambda_Free_RPO_App.thy"] error: keyword "begin" expected, but string was found: "\<ge>t" ^ The error(s) above occurred for theory "Lambda_Free_RPOs.Lambda_Free_RPO_App" (required by "Lambda_Free_RPOs.Lambda_Free_RPOs") (line 11 of "/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_RPOs/Lambda_Free_RPOs.thy") [ line 14 of "/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_RPOs/Lambda_Free_RPO_Std.thy"] error: keyword "begin" expected, but string was found: "\<ge>t" ^ The error(s) above occurred for theory "Lambda_Free_RPOs.Lambda_Free_RPO_Std" (required by "Lambda_Free_RPOs.Lambda_Free_RPOs" via "Lambda_Free_RPOs.Lambda_Free_RPO_Optim") (line 9 of "/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_RPOs/Lambda_Free_RPO_Optim.thy") The error(s) above occurred in session "Lambda_Free_RPOs" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_RPOs/ROOT") Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/UpDown_Scheme/Probability.thy" The error(s) above occurred for theory "UpDown_Scheme.Probability" (required by "UpDown_Scheme.Grid_Point") (line 4 of "/Users/lp15/isabelle/afp/devel/thys/UpDown_Scheme/Grid_Point.thy") No such file: "/Users/lp15/isabelle/afp/devel/thys/UpDown_Scheme/Probability.thy" The error(s) above occurred in session "UpDown_Scheme" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/UpDown_Scheme/ROOT") _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

**
smime.p7s**

*Description:* S/MIME Cryptographic Signature

_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev