drwxr-xr-x |
|
|
[up]
|
|
drwxr-xr-x |
|
|
Cancellation
|
files
|
drwxr-xr-x |
|
|
Sum_of_Squares
|
files
|
drwxr-xr-x |
|
|
Tools
|
files
|
drwxr-xr-x |
|
|
document
|
files
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
28481 |
AList.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
5169 |
AList_Mapping.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
399 |
Adhoc_Overloading.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
400 |
BNF_Axiomatization.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
8771 |
BNF_Corec.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
29440 |
BigO.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
16882 |
Bourbaki_Witt_Fixpoint.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
4072 |
Cancellation.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
15047 |
Cardinality.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
684 |
Case_Converter.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
1473 |
Char_ord.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
4462 |
Code_Abstract_Nat.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
4710 |
Code_Binary_Nat.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
5758 |
Code_Cardinality.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
8949 |
Code_Lazy.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
537 |
Code_Prolog.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
5956 |
Code_Real_Approx_By_Float.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
4049 |
Code_Target_Int.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
5552 |
Code_Target_Nat.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
278 |
Code_Target_Numeral.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
590 |
Code_Target_Numeral_Float.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
5901 |
Code_Test.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
2107 |
Combine_PER.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
9338 |
Comparator.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
78343 |
Complete_Partial_Order2.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
1237 |
Complex_Order.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
1506 |
Conditional_Parametricity.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
4287 |
Confluence.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
9875 |
Confluent_Quotient.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
10688 |
Countable.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
13084 |
Countable_Complete_Lattices.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
21129 |
Countable_Set.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
29720 |
Countable_Set_Type.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
6917 |
DAList.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
16172 |
DAList_Multiset.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
4081 |
Datatype_Records.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
1226 |
Debug.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
4063 |
Diagonal_Subsequence.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
12758 |
Discrete.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
2375 |
Disjoint_FSets.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
25890 |
Disjoint_Sets.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
11809 |
Dlist.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
9153 |
Dual_Ordered_Lattice.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
28914 |
Equipollence.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
5170 |
Extended.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
23781 |
Extended_Nat.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
92236 |
Extended_Nonnegative_Real.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
163892 |
Extended_Real.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
54888 |
FSet.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
11442 |
Finite_Lattice.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
52284 |
Finite_Map.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
96699 |
Float.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
3578 |
Fun_Lexorder.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
30076 |
FuncSet.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
6677 |
Function_Algebras.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
1765 |
Function_Division.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
6234 |
Going_To_Filter.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
12839 |
Groups_Big_Fun.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
7877 |
IArray.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
9050 |
Indicator_Function.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
25303 |
Infinite_Set.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
33346 |
Interval.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
14492 |
Interval_Float.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
5731 |
LaTeXsugar.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
106220 |
Landau_Symbols.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
18626 |
Lattice_Algebras.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
13708 |
Lattice_Constructions.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
7837 |
Lexord.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
1516 |
Library.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
27230 |
Liminf_Limsup.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
32261 |
Linear_Temporal_Logic_on_Streams.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
4109 |
ListVector.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
2825 |
List_Lenlexorder.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
3244 |
List_Lexorder.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
10726 |
Log_Nat.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
10402 |
Lub_Glb.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
40060 |
Mapping.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
2252 |
Monad_Syntax.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
14009 |
More_List.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
152422 |
Multiset.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
20493 |
Multiset_Order.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
13147 |
Nat_Bijection.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
15445 |
Nonpos_Ints.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
19304 |
Numeral_Type.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
15329 |
Old_Datatype.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
2385 |
Old_Recdef.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
32207 |
Omega_Words_Fun.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
5559 |
Open_State_Syntax.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
18193 |
Option_ord.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
2313 |
OptionalSugar.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
18615 |
Order_Continuity.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
1618 |
Parallel.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
7669 |
Pattern_Aliases.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
5466 |
Periodic_Fun.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
1236 |
Phantom_Type.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
69050 |
Poly_Mapping.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
2345 |
Power_By_Squaring.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
10047 |
Predicate_Compile_Alternative_Defs.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
365 |
Predicate_Compile_Quickcheck.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
1907 |
Prefix_Order.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
2822 |
Preorder.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
3359 |
Product_Lexorder.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
9701 |
Product_Order.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
3372 |
Product_Plus.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
6969 |
Quadratic_Discriminant.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
6834 |
Quotient_List.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
2477 |
Quotient_Option.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
3680 |
Quotient_Product.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
3592 |
Quotient_Set.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
2907 |
Quotient_Sum.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
318 |
Quotient_Syntax.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
6930 |
Quotient_Type.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
8670 |
RBT.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
152877 |
RBT_Impl.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
7490 |
RBT_Mapping.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
28805 |
RBT_Set.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
2666 |
README.html
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
45672 |
Ramsey.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
375 |
Realizers.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
1144 |
Reflection.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
6542 |
Refute.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
923 |
Rewrite.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
6537 |
Saturated.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
13793 |
Set_Algebras.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
24735 |
Set_Idioms.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
7635 |
Signed_Division.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
286 |
Simps_Case_Conv.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
22410 |
Sorting_Algorithms.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
8344 |
State_Monad.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
22854 |
Stream.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
57438 |
Sublist.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
2960 |
Subseq_Order.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
602 |
Sum_of_Squares.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
8225 |
Transitive_Closure_Table.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
15675 |
Tree.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
1735 |
Tree_Multiset.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
4280 |
Tree_Real.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
3193 |
Type_Length.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
9175 |
Uprod.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
18301 |
While_Combinator.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
168708 |
Word.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
7526 |
Z2.thy
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
8342 |
adhoc_overloading.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
21695 |
case_converter.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
8500 |
cconv.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
25141 |
code_lazy.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
20147 |
code_test.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
20290 |
conditional_parametricity.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
11407 |
datatype_records.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
1293 |
multiset_simprocs.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
111668 |
old_recdef.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
148004 |
refute.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
17067 |
rewrite.ML
|
file |
revisions |
annotate
|
-rw-r--r-- |
2021-12-04 20:30 +0000 |
4655 |
simps_case_conv.ML
|
file |
revisions |
annotate
|