equal
deleted
inserted
replaced
1993 |
1993 |
1994 definition ferrack_test :: "unit \<Rightarrow> fm" where |
1994 definition ferrack_test :: "unit \<Rightarrow> fm" where |
1995 "ferrack_test u = linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0))) |
1995 "ferrack_test u = linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0))) |
1996 (E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))" |
1996 (E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))" |
1997 |
1997 |
|
1998 code_reserved SML oo |
|
1999 |
1998 ML {* @{code ferrack_test} () *} |
2000 ML {* @{code ferrack_test} () *} |
1999 |
2001 |
2000 oracle linr_oracle = {* |
2002 oracle linr_oracle = {* |
2001 let |
2003 let |
2002 |
2004 |