1033 ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy \ |
1033 ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy \ |
1034 ex/Normalization_by_Evaluation.thy ex/Numeral_Representation.thy \ |
1034 ex/Normalization_by_Evaluation.thy ex/Numeral_Representation.thy \ |
1035 ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \ |
1035 ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \ |
1036 ex/Quicksort.thy ex/ROOT.ML \ |
1036 ex/Quicksort.thy ex/ROOT.ML \ |
1037 ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy \ |
1037 ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy \ |
1038 ex/SAT_Examples.thy ex/Serbian.thy ex/Set_Theory.thy \ |
1038 ex/SAT_Examples.thy ex/Serbian.thy \ |
1039 ex/Simproc_Tests.thy ex/SVC_Oracle.thy \ |
1039 ex/Set_Comprehension_Pointfree_Tests.thy ex/Set_Theory.thy \ |
1040 ex/Seq.thy ex/Sqrt.thy ex/Sqrt_Script.thy \ |
1040 ex/Simproc_Tests.thy ex/SVC_Oracle.thy \ |
|
1041 ex/Seq.thy ex/Sqrt.thy ex/Sqrt_Script.thy \ |
1041 ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy \ |
1042 ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy \ |
1042 ex/Transfer_Int_Nat.thy \ |
1043 ex/Transfer_Int_Nat.thy \ |
1043 ex/Tree23.thy ex/Unification.thy ex/While_Combinator_Example.thy \ |
1044 ex/Tree23.thy ex/Unification.thy ex/While_Combinator_Example.thy \ |
1044 ex/document/root.bib ex/document/root.tex ex/svc_funcs.ML \ |
1045 ex/document/root.bib ex/document/root.tex ex/svc_funcs.ML \ |
1045 ex/svc_test.thy ../Tools/interpretation_with_defs.ML |
1046 ex/svc_test.thy ../Tools/interpretation_with_defs.ML \ |
|
1047 ex/set_comprehension_pointfree.ML |
1046 @$(ISABELLE_TOOL) usedir $(OUT)/HOL ex |
1048 @$(ISABELLE_TOOL) usedir $(OUT)/HOL ex |
1047 |
1049 |
1048 |
1050 |
1049 ## HOL-Isar_Examples |
1051 ## HOL-Isar_Examples |
1050 |
1052 |