drwxr-xr-x |
|
|
[up]
|
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
1395 |
Antiquote.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
40056 |
Argo_Examples.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
6623 |
Arith_Examples.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
14259 |
Ballot.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
14685 |
BinEx.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
4563 |
Birthday_Paradox.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
2275 |
Bubblesort.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
14580 |
CTL.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
7524 |
Cartouche_Examples.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
689 |
Case_Product.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
964 |
Chinese.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
34606 |
Classical.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
1194 |
Code_Binary_Nat_examples.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
6398 |
Code_Lazy_Demo.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
1260 |
Code_Timing.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
4782 |
Coercion_Examples.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
2063 |
Computations.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
1665 |
Conditional_Parametricity_Examples.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
5705 |
Cubic_Quartic.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
1739 |
Datatype_Record_Examples.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
6804 |
Erdoes_Szekeres.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
1124 |
Eval_Examples.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
2059 |
Executable_Relation.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
4297 |
Execute_Choice.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
18017 |
Function_Growth.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
25669 |
Gauge_Integration.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
10851 |
HarmonicSeries.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
1463 |
Hebrew.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
1103 |
Hex_Bin_Examples.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
1166 |
IArray_Examples.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
739 |
Interpretation_in_nested_targets.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
10232 |
Intuitionistic.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
1139 |
Join_Theory.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
2040 |
Lagrange.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
2949 |
List_to_Set_Comprehension_Examples.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
28445 |
LocaleTest2.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
1424 |
MergeSort.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
204986 |
Meson_Test.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
944 |
MonoidGroup.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
2171 |
Multiquote.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
3333 |
NatSum.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
5796 |
Normalization_by_Evaluation.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
2004 |
Note_on_signed_division_on_words.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
8717 |
PER.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
3899 |
Parallel_Example.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
3985 |
Peano_Axioms.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
9708 |
Perm_Fragments.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
3870 |
PresburgerEx.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
1042 |
Pythagoras.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
1160 |
Quicksort.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
4158 |
Radix_Sort.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
21118 |
Reflection_Examples.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
19051 |
Refute_Examples.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
2145 |
Residue_Ring.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
13321 |
SAT_Examples.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
5121 |
SOS.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
11406 |
SOS_Cert.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
5388 |
Serbian.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
5399 |
Set_Comprehension_Pointfree_Examples.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
9090 |
Set_Theory.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
35977 |
Simproc_Tests.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
3775 |
Simps_Case_Conv_Examples.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
5086 |
Sketch_and_Explore.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
2138 |
Sorting_Algorithms_Examples.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
1850 |
Specifications_with_bundle_mixins.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
2212 |
Sqrt_Script.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
10622 |
Sudoku.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
27488 |
Tarski.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
7275 |
Termination.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
7859 |
ThreeDivides.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
4755 |
Transfer_Debug.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
6821 |
Transfer_Int_Nat.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
733 |
Transitive_Closure_Table_Ex.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
18843 |
Tree23.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
2886 |
Triangular_Numbers.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
34636 |
Unification.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
2080 |
While_Combinator_Example.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
5230 |
Word_Lsb_Msb.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2023-01-14 23:50 +0100 |
17230 |
veriT_Preprocessing.thy
|
file |
revisions |
annotate
|