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

Reply via email to